Формальная разработка систем

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

Рис. 3.3. Модель формальной разработки ПО

Между данным подходом и каскадной моделью существуют следующие кардинальные отличия.

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

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

Рис. 3.4. Процесс формальных преобразований

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

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

Наиболее известным примером метода формальных преобразований является метод "чистой комнаты" (Cleanroom), разработанный компанией IBM [239, 310, 219, 284]. Этот метод предполагает пошаговую разработку ПО, когда на каждом шаге применяется формальные преобразования. Это позволяет отказаться от тестирования отдельных программных модулей, а тестирование всей системы происходит после ее сборки. Этот подход более подробно рассмотрен в главе 19.

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

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