Формальные спецификации ПО

Цели

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

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

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

q иметь представление о том, как формальные методы можно использовать для специфицирования поведения системы.

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

Термин "формальные методы" подразумевает ряд операций, в состав которых входят создание формальной спецификации системы, анализ и доказательство спецификации, реализация системы на основе преобразования формальной спецификации в программы (см. главу 3) и верификация программ. Все эти действия зависят от формальной спецификации программного обеспечения. Формальная спецификация – это системная спецификация, записанная на языке, словарь, синтаксис и семантика которого определены формально. Необходимость формального определения языка предполагает, что этот язык основывается на математических концепциях. Здесь используется область математики, которая называется дискретной математикой и основывается на алгебре, теории множеств и алгебре логики.

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

Теперь ясно, что эти предсказания не сбылись, причем по целому ряду причин.

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

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

3. Ограниченная область применения формальных методов. Формальные методы обычно плохо подходят для описания взаимодействий пользователя и определения пользовательских интерфейсов. Пользовательские интерфейсы являются составной частью большинства современных систем, здесь польза от применения формальных методов ограниченна.

4. Ограниченная масштабируемость формальных методов. В успешных проектах формальные методы, как правило, использовались для разработки только относительно небольшого критического ядра системы. Проблема усугубляется недостатком средств поддержки таких методов.

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

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

Примерами критических систем, при разработке которых успешно применялись формальные методы, являются информационные системы управления воздушным транспортом [148], системы сигнализации на железной дороге [90], бортовые системы космических кораблей [102] и медицинские системы управления [183, 185]. Они также были использованы для специфицирования пакетов программных средств [253], части системы CICS (абонентская информационно-управляющая система) компании IBM [349] и ядра систем, работающих в режиме реального времени [324]. Метод "чистой комнаты" разработки ПО [239, 219, 284], который рассмотрен в главе 19, основывается на формальных доказательствах того, что программа соответствует своей спецификации.