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

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

Задачи изучения тем:

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

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

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

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

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

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

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

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

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

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

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

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

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

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