Корректность — одно из ключевых свойств ПО, а методы проверки и обеспечения корректности — важная и актуальная область исследований в инженерии программного обеспечения Выделяются два основных подхода к проверке корректности: динамический и статический. При динамическом подходе программа проверяется в процессе исполнения. Наиболее употребительным примером применения этого подхода является тестирование программ. В настоящее время в области тестирования проводится множество исследований, цель которых — автоматизация процесса тестирования, повышение вероятности нахождения ошибок и т. д. Таким образом, тестирование позволяет находить все больше и больше ошибок, однако, как отметил Э. Дейкстра, оно никогда не сможет гарантировать корректность программы. Напротив, статические методы проверки гарантируют правильность программы в том или ином смысле. Простейший вид статической проверки (проверка синтаксиса программного текста) существует в любом компиляторе. На следующем уровне находится так называемая валидация: контроль за выполнением более сложных свойств программной системы, таких как, например, типовая корректность. Валидация выполняется большинством современных сред разработки, если язык программирования это предусматривает (в частности, имеет статическую систему типов). Наиболее мощным видом статической проверки корректности является формальная верификация — доказательство соответствия текста программной системы набору свойств, описанному на некотором формальном языке. Этот набор свойств обычно называют формальной спецификацией системы. В рамках формальной верификации выделяются два основных направления: доказательная верификация и проверка модели программы (Model Checking) Доказательная верификация, как правило, требует большого объема ручной работы, что делает ее малоприменимой для программных систем большого размера. Для верификации модели программы необходимо решить следующие задачи: построить по программе модель с конечным числом состояний и формально описать требования к программе в терминах одного из видов темпоральной логики В результате верификации модели либо подтверждается, что модель удовлетворяет формализованным требованиям, либо строится контрпример. В последнем случае требуется определить причину некорректности: ошибка в исходной программе, в спецификации или при построении модели. При этом необходимо решить задачу переноса контрпримера из модели в исходную программу. Для программ общего вида решение этих задач плохо поддается автоматизации. Переходя к автоматным программам, остановимся сначала на динамической проверке их корректности. Большинство существующих библиотек и инструментальных средств, поддерживающих автоматное программирование, позволяют вести протокол выполнения программы в терминах автоматов. В этом протоколе записывается последовательность состояний, в которых пребывал автомат, обработанные события, значения входных и выходных переменных, а при помощи специального форматирования (например, отступов) наглядно отражаются отношения вложенности и вызываемости между автоматами Кроме того, как было упомянуто выше, инструментальное средство UniMod позволяет осуществлять пошаговую отладку в терминах автоматов. Применяя описанные высокоуровневые средства отладки, гораздо проще находить ошибки в логике сложного поведения, чем с использованием традиционных методов. Что касается статической проверки корректности, для автоматных программ существуют специфические методы, которые также можно отнести к нескольким уровням. На простейшем, синтаксическом уровне выделяются такие правила, как, например, «Любой переход должен вести из одного состояния в другое». На уровне валидации существует целый ряд поведенческих свойств, которые несложно проверить по графу переходов автомата. Это позволяет устранить программные ошибки, которые было бы трудно обнаружить без использования автоматного подхода. Достижимость. В любое состояние автомата должен вести путь из начального состояния, составленный из переходов. В противном случае это состояние не имеет смысла, так как автомат никогда не сможет в нем оказаться. Само по себе недостижимое состояние безвредно, однако оно, скорее всего, свидетельствует об ошибке при построении автомата. Непротиворечивость. Множество переходов из каждого состояния автомата должно быть непротиворечивым: не должно существовать такого входного воздействия, при котором условия нескольких переходов из этого множества будут одновременно истинными. При использовании распространенных методов программной реализации автоматов наличие противоречия приведет к тому, что будет выбран один из переходов, однако какой именно, невозможно определить по диаграмме. Такой недетерминизм не несет практической пользы и, как правило, также свидетельствует об ошибке. Полнота. Множество переходов из каждого состояния автомата должно быть полным: для любого входного воздействия должен существовать хотя бы один переход из этого множества, условие которого будет истинным. При отсутствии этого свойства невозможно гарантировать правильную работу автоматной программы, так как во время выполнения может сложиться ситуация, когда автомат не сможет совершить переход. Таким образом, функционирование всей автоматной модели будет нарушено.
Отметим, что перечисленные выше свойства проверяются формально, без учета семантики входных и выходных переменных. Обычно этого оказывается достаточно. Однако если объект управления наделен формальной спецификацией, ее можно принять во внимание при проверке свойств автомата. Например, в спецификации может быть указано, что некоторые входные переменные не могут быть одновременно истинными. Такая информация способна повлиять на результаты проверки всех трех перечисленных свойств. Перейдем теперь к формальной верификации автоматных программ. В этой области в настоящее время активно ведутся исследования в России Специфическая структура автоматных программ, в которых запросы и команды объекта управления представляют собой очень простые подпрограммы, а логика сложного поведения описана конечными автоматами, как это делается при использовании инструментального средства UniMod позволяет совместно использовать оба указанных выше подхода к формальной верификации. Для простых подпрограмм (компонентов объекта управления) целесообразно использовать доказательный подход, а управляющие автоматы могут быть формально преобразованы в модель с конечным числом состояний, которая подлежит верификации методом Model Checking. Это преобразование может быть автоматизировано. Также может быть автоматизировано и обратное преобразование в случае, если верификатор построил контр пример. Для автоматных UniMod-программ не существует семантического разрыва между требованиями к программе и модели — он преодолевается в процессе проектирования автоматов. В настоящее время существуют экспериментальные реализации инструментов, которые позволяют весьма эффективно проводить верификацию автоматных программ указанного класса Результаты работ по верификации автоматных программ на основе метода Model Checking, полученные под руководством одного из авторов книги в ходе выполнения государственного контракта, приведены по адресу http://is.ifmo.ru/verification/.Упрощение формальной верификации автоматных программ по сравнению с программами, написанными без явного выделения управляющих состояний, позволяет авторам надеяться, что со временем в технических заданиях на проектирование ответственных программных систем будет указано на необходимость использования автоматного подхода.