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

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

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

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

Рис. 9.1. Разработка спецификации и проектирование

Рис. 9.2. Разработка формальной спецификации

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

Разработка и анализ формальной спецификации требуют дополнительных затрат. На рис. 9.3 показана стоимость создания ПО при разработке формальной спецификации и без нее. При обычном процессе разработки ПО стоимость аттестации системы составляет около 50% всей стоимости разработки, а стоимость проектирования и реализации системы в два раза больше стоимости разработки спецификации. При использовании формальной спецификации стоимости разработки спецификации и реализации системы соизмеримы, а стоимость аттестации значительно снижается, поскольку в процессе разработки формальной спецификации обнаруживаются и устраняются недоработки в требованиях, тем самым исключается переделка системы на последних стадиях ее создания.

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

1. Алгебраический подход, при котором система описывается в терминах операций и их отношений.

2. Подход, ориентированный на моделирование, при котором модель системы строится с использованием математических конструкций, таких, как множества и последовательности, а системные операции определяются тем, как они изменяют состояния системы.

Рис. 9.3. Стоимость разработки ПО с формальной спецификацией

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

Таблица 9.1. Языки разработки формальных спецификаций