Как получить бездефектную систему?

Три из шести больших статей номера посвящены разным проблемам программной инженерии, хотя эту часть номера вряд ли можно считать полноценной тематической подборкой – слишком широка тематика и отсутствует приглашенный редактор. Первая статья называется «Бездефектные системы: да, мы можем добиться этого!» (Faultless Systems: Yes We Can!) и написана Жаном-Раймоном Эбриэлем (Jean-Raymond Abrial).

Статья умышленно названа провокационно. Все знают, что бездефектные системы невозможны, иначе их давно бы производили. И что такое «дефект»? Автор стремится напомнить несколько простых фактов и идей, которые могут пригодиться разработчикам программного обеспечения. При возникновении ужасной ситуации проявления дефектов в программной системе можно было бы попытаться радикально изменить положение вещей, но это никогда не получается – предложение автора состоит в поэтапном применении некоторых простых приемов, которые в совокупности позволяют, в конце концов, облегчить ситуацию.

Прежде всего, для создания корректных систем необходимо строго определить способ оценки корректности. В этом состоит основное назначение документа, описывающего требования к системе, – такой документ должен быть тщательно написан еще до того, как предпринимаются какие-либо шаги к разработке системы. Однако в конце фазы документирования требований к будущей системе отсутствуют гарантии их удовлетворения. Ошибка состоит в немедленном переходе к фазе программирования, состоящего в создании некоторого фрагмента формального текста, указывающего компьютеру, как следует выполнять определенные задачи, однако целью разработчиков является построение системы, в которой будет присутствовать много таких взаимодействующих фрагментов. Разработчикам нужно понять, как будет функционировать система в целом, и для этого необходимо выполнить ее полное моделирование, включая программное обеспечение и среду его выполнения.

Моделирование обеспечивает формализацию мысленного представления будущей системы и позволяет доказать, что это представление обеспечивает определенные свойства, зафиксированные в требованиях к системе. Для выполнения этой общей задачи симуляции и доказательств используется простой формализм дискретных систем переходов. Другими словами, компоненты будущих систем всегда представляются через последовательности состояний, тесно сплетенных со скачкообразными переходами – событиями.

С модельной точки зрения нет существенной разницы между человеком, нажимающим на некоторую кнопку, запуском или остановкой мотора или фрагментом программы, выполняющим некоторые задачи, – все эти события происходят в одной и той же системе. Каждая из этих активностей является некоторой дискретной системой переходов, работающей сама по себе и взаимодействующей с другими активностями. Эта простая парадигма оказывается исключительно полезной. В частности, задача доказательства частично решается путем демонстрации того, что переходы в любом компоненте не нарушают некоторые общие свойства системы. Эти свойства называются «инвариантами», а соответствующие доказательства – «доказательствами сохранности инвариантов».

Чтобы доказать соответствие программы требованиям, нужно конструировать эту программу путем моделирования проблемы.

Внедрены ли в практику обсуждаемые в статье простые и известные идеи, автор отвечает умеренно положительно: бездефектные системы существуют, однако требуется ряд дополнительных шагов, чтобы эти идеи были более широко осознаны и приняты к действию. И на это направлен европейский проект Deploy (www.deploy-project.eu).

Авторы следующей статьи – Сью Блэк (Sue Black), Пол Бока (Paul Boca), Джонатан Боуэн (Jonathan Bowen), Джейсон Горман (Jason Gorman) и Майк Хинчи (Mike Hinchey). Статья называется «Формальные и быстрые методы: выживут наиболее пригодные?» (Formal Versus Agile: Survival of the Fittest?).

Программная инженерия как самостоятельная дисциплина прошла в своем развитии несколько фаз:

• переход от инженерии аппаратного оборудования в 50-е годы к кустарному программированию в 60-е;
• введение формализованности и каскадного процесса (waterfall process) разработки программного обеспечения в 70-е годы;
• появление приемов повышения производительности и масштабируемости труда программистов в 80-е годы;
• введение параллельных процессов разработки в 90-е годы;
• возникновение скорых (agile) процессов в 2000-е годы.

Каждая следующая фаза оказывалась развитием предыдущей фазы или реакцией на ее недостатки.

По утверждению авторов, появление формальных методов следует связывать с работами Чарльза Бэббиджа и Ады Лавлейс над разностными и аналитическими машинами. Понятие корректности присутствовало уже на этой доэлектронной фазе – Бэббидж писал о «верификации формул, размещенных на технологических картах», а Алан Тьюринг одним из первых воспользовался формальными методами в своей статье о корректности программ (www.turingarchive.org/browse.php/B/8). Однако в терминологию программной инженерии формальные методы вошли только в 70-е годы.

По сравнению с формальными методами методология скорой разработки сравнительно нова. В 2001 году в Agile Manifesto (agilemanifesto.org) были выдвинуты четыре основных принципа этого подхода:

• реагировать на изменения важнее, чем следовать плану;
• люди и их взаимодействие важнее процессов и средств;
• работающее программное обеспечение важнее исчерпывающей документации;
• сотрудничество с заказчиком важнее обсуждения условий контракта.

Возникновение методологии скорой разработки можно считать реакцией на громоздкую каскадную модель, которая фокусировалась на формализации требований заказчика в начале жизненного цикла программного продукта и доставке готового продукта в конце этого цикла, без каких-либо взаимодействий с заказчиком в середине цикла. Считалось, что быстрые методы лучше всего подходят для небольших групп умных программистов, но это слишком ограничивает область их применения.

Сравнительно недавно возникло направление исследований по интеграции формальных и быстрых методов. На прошедшем в 2003 году Первом южноевропейском симпозиуме по формальным методам (delab.csd.auth.gr/bci1/SEEFM03) обсуждались новые формальные методы, интеграция формальных и быстрых методов и проблемы оценки «быстроты» формальных методов.

Последняя статья тематической подборки представлена Бертраном Мейером (Bertrand Meyer), Арно Фивой ( Arno Fiva), Илинкой Чупа (Ilinca Ciupa), Андреасом Лейтнером (Andreas Leitner), Йи Веем (Yi Wei) и Эммануэлем Стапфом (Emmanuel Stapf) и называется «Программы, которые тестируют сами себя» (Programs That Test Themselves).

Современные технические продукты – от самолетов, автомашин и промышленных установок до холодильников и кофеварок – регулярно тестируют сами себя во время эксплуатации. Эта возможность с самого начала разработки, но, чтобы добиться такой возможности, нужно проектировать изделие в расчете на их тестируемость, что не всегда применялось. Например, в автомобилях раньше обычно отсутствовали какие-либо индикаторы, указывающие на появление серьезных проблем, и при желании узнать больше о состоянии своего автомобиля нужно было обращаться к специалисту, который подряд проверял все компоненты, не зная, что в действительности происходило во время эксплуатации. Современные автомобили наполнены датчиками и индикаторами, производящими непрерывное тестирование и собирающими данные для технического обслуживания.

Хотя программное обеспечение не изнашивается физически в ходе эксплуатации, при его разработке также требуется обширное тестирование, тем не менее при его проектировании потребностям тестирования во время выполнения сегодня уделяется недостаточное внимание. Разработчики программного обеспечения оказываются глухи к урокам из других областей производства. В результате тестирование, несмотря на совершенствование инструментальных средств, остается трудоемким процессом.

AutoTest (se.ethz.ch/research/autotest) – это набор инструментальных средств, которые автоматизируют процесс тестирования на основе использования программ, содержащих приспособления для своей собственной верификации. Эти приспособления имеют форму контрактов – спецификаций классов и их методов. Три основных компонента AutoTest затрагивают взаимосвязанные аспекты тестирования.

• Генерация тестов. Автоматически создает и выполняет тестовые сценарии без потребности в тестовых сценариях и оракулах, подготовленных вручную.
• Выявление тестов на сбойные ситуации. Идея выявления тестов заключается в том, что некоторые важнейшие тестовые сценарии, по существу, невозможно придумать заранее – они возникают, когда разработчик неформально испытывает программу в ходе ее разработки. Сбойные ситуации представляют интерес, в частности, для будущего регрессионного тестирования, но обычно они не запоминаются. Разработчик устраняет проблему и движется дальше. На основе таких сбойных ситуаций компонент выявления тестов создает тестовые сценарии, которые могут воспроизводиться в будущих тестовых кампаниях.
• Интеграция тестов, создаваемых вручную. Поддерживает разработку таких тестов и управление ими. В отличие от первых двух компонентов, здесь используются общепринятые методы и отсутствуют какие-либо новшества, но обеспечивается единообразное автоматическое управление всеми тестами независимо от их происхождения.

Эти механизмы, разработанные в Федеральной политехнической школе Цюриха (Швейцария) для исследовательских целей, теперь интегрированы в среду EiffelStudio. Доступен как их вариант с открытыми кодами (eiffelstudio.origo.ethz.ch), так и коммерческий продукт.

Первую статью вне тематической подборки – она названа «Динамическая конфиденциальность при общественных видеонаблюдениях» (Dynamic Privacy in Public Surveillance) – написали Саймон Монкрайф (Simon Moncrieff), Света Венкатеш (Svetha Venkatesh) и Джеф Вест (Geoff West).

В последние годы исследователи много обсуждают вопросы конфиденциальности и ее влияния на повсеместную компьютеризацию. Хотя никто не спорит с тем, что поддержка конфиденциальности в «вездесущих компьютерных системах» (ubiquitous computing) необходима, эта область все еще находится в зачаточном состоянии. Пока еще сравнительно редко речь идет о системах, в которых были бы использованы идеи вездесущего компьютинга. Наиболее известна система Privacy Protected Video Surveillance (Privacy Cam), разработанная Эндрю Сениором (Andrew Senior) и его коллегами.

Однако скоро эта ситуация изменится. Последние достижения в технологии видеонаблюдений, такие как цифровые сетевые видеокамеры и решения для длительного хранения видеоданных, расширяют область применения сред видеонаблюдения, превращая зафиксированные фрагменты видео в индексируемые данные, над которыми можно производить поиск. Это приведет к усилению посягательств на конфиденциальность, что, в свою очередь, повысит потребность в реализации средств поддержки конфиденциальности, контролирующих доступ к данным видеонаблюдений.

Для обеспечения эффективности телевизионные системы с закрытой передачей (Closed-Circuit Television, CCTV) должны быть интегрированы в общую конструкцию системы видеонаблюдений. Кроме того, политики конфиденциальности должны динамически изменяться в зависимости от обстановки, чтобы обеспечивать максимальную конфиденциальность, не препятствуя достижению основных целей системы.

Авторами статьи «Применение принципов Парнаса на новом уровне: разработка декларативного языка» (Taking Parnas’s Principles to the Next Level: Declarative Language Design) являются Дэниэл Кук (Daniel Cooke) и Нельсон Раштон (Nelson Rushton).

В течение последних 17 лет авторы экспериментировали с декларативными подходами к организации вычислений над нескалярными значениями. Эти исследования привели к разработке языка SequenceL, который полон по Тьюрингу и компактен (12 грамматических правил по сравнению c более чем 120 в языке Java), а его семантика основывается на двух вычислительных законах CSP-NT: «потребляй-упрощай-производи» (consume-simplify-produce) и «нормализуй-преобразуй» (normalize-transpose). Было разработано около десятка интерпретаторов и четыре кодогенератора для компиляции SequenceL в языки программирования Cи и C++. Один из последних кодогенераторов использовался для приложений дистанционного наведения, навигации и управления в тренажерах челноков NASA и пилотируемого космического аппарата Orion. Генератор код SequenceL обеспечивает производительность рабочих программ, сравнимую с производительностью приложений, написанных инженерами NASA вручную. В лучших случаях откомпилированные SequenceL-программы выполняются быстрее своих двойников на Cи; в худших – проигрывают им в производительности в 2,1 раза. В настоящее время один из интерпретаторов перерабатывается с целью генерации многопотокового кода для многоядерных процессоров.

В последнее время авторы принимают участие в эксперименте по переписыванию приложений одной из крупных компаний, специализирующейся на управлении производственными процессами. Этот эксперимент должен продемонстрировать повышение производительности труда программистов благодаря декларативному характеру SequenceL и рост эффективности приложений из-за параллельного выполнения.

В статье авторы демонстрируют, как можно применить к разработкам принципы обеспечения программиста только информацией, требуемой для корректного использования языка, и обеспечения его лишь информацией, требуемой для реализации приложения. Первую цель можно считать успешно достигнутой, если программисту не требуется знание операционной семантики языка, а вторую – если язык не разрабатывается в расчете на конкретную область приложений. Для этого в SequenceL авторы фокусируются на абстракциях и усовершенствованиях, не основанных на семантике, таких как применение правил CSP-NT, которые позволяют описывать алгоритмы решения произвольной заданной проблемы.

Последняя большая статья номера называется «Обеспечение безопасности в небесах: мы верим в требования» (Securing the Skies: In Requirements We Trust). Ее авторами являются Башар Нузейбех (Bashar Nuseibeh), Чарльз Хейли (Charles Haley) и Крейг Фостер (Craig Foster).

Нас регулярно засыпают сообщениями о нарушении конфиденциальности информации, целостности объектов, недоступности продуктов и услуг, а в ответ мы должны быстро выявить дефекты в своих системах. И это вполне справедливо – в конце концов, безопасность направлена на защиту наших систем от нанесения ущерба. Тем не менее, как считают авторы, при разработке безопасного программного обеспечения внимание должно быть направлено на более масштабные системы, в которых программное обеспечение является лишь одной из частей. И именно в этих более крупных социотехнических системах возникают угрозы.

Социотехническая система включает людей, разработчиков, пользователей, аппаратуру, программное обеспечение и организационные структуры, в которых функционируют эти объекты. Хотя компьютерные системы действительно подвергаются атакам, вред наносится пользователям и их активам, поэтому организациям нужно понять, что они пытаются защищать, почему нужно защищать именно это и какими могут быть последствия несовершенной защиты. Набор видов деятельности, помогающих ответить на эти вопросы, называется «инженерией требований к безопасности» (security requirements engineering). Авторы разрабатывали инфраструктуру и соответствующие инструментальные средства для поддержки этих видов деятельности. В исследовании, проведенном Национальной службой воздушного движения Великобритании, эта инфраструктура использовалась для анализа проблем безопасности в новой технологии, предназначавшейся для интеграции существующих систем управления воздушным движением.