Формальные методы
Понятие формальные методы более всего связано с математическими техниками спецификаций, верификации та доказательства правильности создаваемых программ. Эти методы содержат математическую символику, формальную нотацию, аппарат вывода и потому они трудно используются рядовыми программистами. Кроме того, постоянно развиваемые эти средства не вкладываются в стандартизованные процессы ЖЦ, в котором регламентированы все основные и дополнительные процессы (управление качеством, проектом, ресурсами и др.).
За многие годы своего существования (более 20–лет) такие известные формальные методы, как VDM, Z, RAISE [43–46] используются редко, эпизодически в реальных проектах, более всего в университетских и академических организациях и до промышленного производства фактически не дошли.
Это связано с тем, что формальные техники трудно использовать практически особенно в системах реального времени, где особенно важно применение формальных методов для создания более надежных программ, стоимость разработки которых возрастает, так как тратиться много времени на спецификацию и верификацию.
Наука формального проектирования ПС получила значительный прогресс при создании обобщенного UML, который доведен до стандарта, отодвинув на второй план такие средства спецификации, как RAISE, VDM и др.
Далее рассматриваются некоторые техники спецификации моделей программ и методы формального доказательства.
Графова модель VDM создается с помощью композиционной теоремы [5], которая определяется в виде ациклического графа, узлы которого – модули, а дуги – интерфейс между модулями.
Каждому модулю модели соответствует сервис как provider, так и потребителя (consumer) услуг. Дуга графу от модуля M к N определяет интерфейс, который может предоставлять модуль N для модуля M.
Базисом формального метода представления модели есть спецификация интерфейсов модулей для двух выше указанных пользователей сервисов.