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

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

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

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

отличия.

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

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

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

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

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

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

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

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