И. Соммервилл - Инженерия программного обеспечения (1133538), страница 48
Текст из файла (страница 48)
Формальные спецификации ПО е Цель настоящей главы — представить формальные спецификации, которые можно использовать для детализации спецификации системных требований. Прочитав эту главу, вы должны: П понимать, почему методы формальной спецификации помогают обнаруживать проблемы в системных требованиях; 0 знать, как для йюрмировапия требований, описывающих интерфейс, используютса алгебраические методы формальных спецификаций; 0 иметь представление о том, как формальные методы можно использовать для специфицирова.
ния поведения системы. ' о -е'див 9.1. Формальные спецификации в процессе разработки ПО 9.2. Специфицирование интерфейсов 9З, Спецификация поведения систем 188 Часть П. Требования Традиционные технические дисциплины, такие, как электротехника или гражданское строительство, обычно легко адаптируют лучшие математические методы. Например, в машиностроении не возникало трудностей с применением методов математического анализа. Однако инженерия программного обеспечения не идет таким путем. Хотя прошло более 25 лет исследований по использованию математических методов в процессе создания ПО, воздействие этих методов все же ограниченно. Так называемые формальные методы разработки программных систем широко не используются.
Многие компании, рырабатывающие ПО, не считают экономически выгодным применение этих методов в про. цессе разработки. Термин "формальные методы" подразумевает ряд операций, в состав которых входят создание формальной спецификации системы, анализ и доказательство спецификации, реализация системы на основе преобразования формальной спецификации в программы (см. главу 3) и верификация программ.
Все зги действия зависят от формальной спецификации программного обеспечения, Формальная спецификация — это системная спецификация, записанная па языке, словарь, синтаксис и семантика которого определены фор. мально. Необходимость формального определения языка предполагает, что этот язык основывается на математических концепциях.
Здесь используется область математики, которал называется дискретной математикой и основывается иа алгебре, теории мне. жеста и алгебре логики. В 1980-х годах многие исследователи считали. что формальные спецификации и фор. мальпые методы являются наиболее эффективным путем улучшения качества ПО. Они при. вели веские доводы в пользу того, что строгий и детальный анализ, который является неотьемлемой частью формальных методов, приведет к созданию программ с малым количеством ошибок. Они предсюзывали, что к ХХ1 столетию большая часть программного обеспечения будет разрабатываться с использованием формальных методов. Теперь ясно, что эти предсказания не сбылись, причем по целому ряду причин.
1. Уелехи инженерии программного абггэгечеиил. Использование в процессе проектировапил и разработки программных систем таких технологий инженерии ПО, как структурные методы, управление конфигурацией. сокрытие информации и т.д., привело к повышению качества программных продуктов. Зто противоречит бытовавшим представлениям, что повышение качества программ может быть достигнуто только путем доказательства их правильности. 2. Игмгиеиил ил ~ьтхе ирагупммных яуюдухтов. В 1980-х годах качесгво являлось ключевой проблемой в создании ПО. В настоящее время главным критерием при разра. боткс многих классов ПО является не качество, а время поставки его на рынок. Программное обеспечение должно быть разработано быстро, и клиенты готовы примять его с некоторыми дефектами, если будет обеспечена быстрая поставка.
Методы быстрой рюработки ПО не очень хорошо согласуютсл с формальной спецификацией. Конечно, качество является вагиным показателем, но оно должно дос. тигаться в коитексге с быстрой поставкой на рынок. 3. ОгГхггшчеигига абмиив применения ффюгглимхгмамдоа.
Формальные методы обычно плохо подходят для описания юаимодействий пользователя и определения пользовательских интерфейсов. Пользовательские интерфейсы являются составной частью большинства современных систем. здесь польза от применения формальных методов ограниченна. 4. Огрлиичеинал моежиигбируемогтл гдормглгьимх гмжодао. В успешных проектах формальпыс лгетоды, как правило, использовались для разработки только относительно не. большого критического ядра системы, Проблема усугубляется недостатком средств поддержки таких методов. 9.
Формаяьиьге спецификации ПО 189 Эти факторы привели к тому, что риски применения формальных методов в большинстве проектов ПО перевешивают возможные выгоды от их использования. Затраты и проблемы введения формальных методов в процесс разработки очень высоки. Однако формальная спецификация является отличным способом обнаружения ошибок в требованиях и средсгвом, обеспечивающим однозначность системной спецификации. Во всех успешных проектах, использовавших формальные методы, сообщалось об уменьшении ко. личества ошибок в законченных программных сисгемах. Таким образом, в системах, где возможно применение формальных методов, оно может быть оправданным и, вероятно, будет рентабельным. Использование формальных методов возрастает в специальной области разработки критических систем, где очень важны такие свойства, как безопасность, безотказность и защищенность.
Для таких систем, как описанные в части ПГ, аттестация требует больших затрат, а стоимость отказов весьма велика. В этом случае рентабельно использовать формальные методы, поскольку они но~от уменьшить эти затраты. Примерами критических систем, при разработке которых успешно применялись формальные методы, являются информационные системы управления воздушным транспортом [148], снсгемы сигнализации на железной дороге (90], бортовые системы космических кораблей [102] и медицинские системы управления [18Я, 185]. Они также были использованы для специфицирования пакетов программных средств [255], части системы СН.э (абонентская информационноуправляющая система) компании 1ВМ [549] и ядра систем, работающих в режиме реального временп [Я24].
Метод "чистой комнаты" разработки ПО [259, 219, 284], который рассмотрен в главе 19, основывается на формальных доказательствах того, что программа соответствует своей спецификации. 9.1. Формальные спецификации в процессе разработки ПО В главе б определены три уровня спецификации программного обеспечения. Это поль. зовательские и системные требования и спецификация структуры программной системы. Пользовательские требования наиболее обобщенные, спецификация структуры наиболее дстальна.
Формальные математические спецификации находятся где.то между с>штемными требованиями и спецификацией структуры. Они не содержат деталей реализации системы, но должны представлять ее полную математическую модель. По мере разработки спецификации участие заказчика уменьшается, а участие подрядчиков и непосредственно разработчиков ПО возрастает. На ранних стадиях разработки спецификация должна быть "ориентирована на заказчика" и написана так, чтобы он мог ее понять.
Однако на заключительной стадии процесса разработки должна быть получена спецификация, в основном предназначенная для подрядчиков и разработчиков ПО, по. скольку она будет служить основой для реализации сисгемы. Эта конечная спецнфнкацил может быть формальной. На рис. 9.1 показаны этапы разработки спецификации ПО и их взаимосвязи с процессом проекгирования. Этапы разработки спецификации, показанные на рис. 9.1, не явля. ются независимыми и не обязательно разрабатываются в приведенной последовательно. сти. На рис.
9.2 показано, что разработка спецификация н проектирование могут выпол. няться параллельно, когда информация от этапов разработки спецификации передается к этапам проектирования и наоборот. 190 Часть П. Требования Умвишеню учазша заизчаш Разработюа свацафягацва Ркс 9.1. Рпэрпбовгкп спецификации и паоекзшроопкко гркс. 9.2. Рпэрпботкп формальной спезификпзии Создание формальной спецификации требует детального анализа системы, который позволяет обнаружить ошибки и несоответствия в спецификации неформальных требований. Эта воэможность обнаружения ошибок- наиболее важный аргумент для испольэо.
ванна формальной спецификации 1147]. Проблемы в требованиях, которые остаются ие. обнаруженными до последних стадий процесса разработки ПО, обычно требуют больших затрат на исправление. Разработка и анализ формальной спецификации требуют дополнительных затрат. На рис. 9.3 показана стоимость создания ПО при разработке формальной спецификации и без нее.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
