обычно могут быть верифицированы без построения более
абстрактных моделей.
Таким образом, автоматные программы в значительной мере можно
верифицировать автоматически. Для таких программ нет
необходимости строить модель для верификации и вручную
возвращаться из модели в программу при нахождении контрпримера.
Это является большим их преимуществом по сравнению с
программами, построенными традиционным путем. Эффективность
верификации часто обратна эффективности программ, которые
верифицируются. Автоматные программы обычно не являются
эффективными в традиционном понимании, однако, как будет
показано ниже, они весьма просто верифицируются с помощью
проверки моделей. Поэтому возможно, что со временем в технических
заданиях на создание ответственных систем, которые необходимо
верифицировать, будет записано, что программы для них следует
проектировать на основе автоматного подхода. Уже сегодня этот
подход для некоторых классов таких систем постоянно применяется
[56, 57].
Известно, что если схемы не контролепригодны, то их нельзя
проверить, и это, например, при проектировании микропроцессоров,
понимают все. Поэтому возможность проведения контроля
закладывается в схему при ее проектировании. В программировании
ситуация складывается иначе: программа пишется по определенным
законам, обычно далеким от обеспечения возможности ее
верификации. При этом на практике, даже если известно, что
программу надо будет верифицировать, подходов к ее созданию не
изменяют, и поэтому верификация управляющих аспектов поведения
программы обычно трудоемка.
Проверка моделей после своего появления начала применяться как
наиболее практичный метод из известных, но и здесь имеет место не
вполне естественная ситуация: не известно ни одной области
техники,, в том числе и для серийной продукции, в которой сначала
объект реализуется, а затем для него разрабатывается модель. Обычно
при создании практически любого образца техники все в нем
спроектировано заранее. Трудно представить себе, чтобы кто-то в
промышленности изготовил автомобиль, самолет или подводную
лодку, а потом начал создавать модели и выпускать чертежи. Но в
программировании при использовании проверки моделей обычно
именно так и поступают: сначала создается программа, а потом
строится ее модель. В автоматном программировании ситуация
противоположная и более естественная.