Формальные методы

Понятие формальные методы более всего связано с математическими техниками спецификаций,  верификации та доказательства правильности создаваемых программ. Эти методы  содержат математическую символику, формальную нотацию, аппарат вывода   и потому они трудно используются рядовыми программистами. Кроме того,  постоянно развиваемые эти средства не вкладываются в  стандартизованные процессы ЖЦ, в котором регламентированы все основные и дополнительные процессы (управление качеством, проектом, ресурсами и др.).

За многие годы своего существования (более 20–лет) такие известные формальные методы, как VDM, Z, RAISE [43–46]  используются редко, эпизодически в реальных проектах, более всего в университетских и академических организациях и до промышленного производства фактически не дошли.

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

Наука формального проектирования ПС получила значительный прогресс при создании обобщенного UML, который доведен до стандарта, отодвинув на второй план такие средства спецификации, как RAISE, VDM и др.

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

Графова модель VDM создается  с помощью  композиционной теоремы [5], которая  определяется в виде ациклического графа,  узлы которого – модули, а дуги – интерфейс между модулями.

Каждому модулю модели соответствует сервис как provider, так и потребителя (consumer) услуг. Дуга графу от модуля M к N определяет интерфейс, который может предоставлять модуль N для  модуля M.

Базисом формального метода представления модели есть спецификация интерфейсов модулей для двух выше указанных пользователей сервисов.