конечные автоматы для верификации

[juan_gandhi]

Тут в разговоре про очередного, имхо, шарлатана, профессора Шалыто, выяснилось, что есть такая идея, будто для верификации программ достаточно FSM, конечного автомата.

Вот скажите мне, возьмём такой пример: даден алфавит, {a, b}, и две программы, одна генерирует все палиндромы в этом алфавите, вторая проверяет, что данная строка является палиндромом.

Скажите, какой конечный автомат может верифицировать эти программы?

Comments

[dtim.livejournal.com]

Там как бы не совсем обычные автоматы, там автоматы, работающие с бесконечными цепочками (например, Büchi automaton). Но количество состояний конечно, да. При этом нет задачи смоделировать поведение программы конечным автоматом: вместо этого поведение системы представляется в виде цепочки символов, и множества таких цепочек задаются с помощью автоматов.

Идея примерно такая. Сначала формулируем свойство, которое хочется проверить. Затем, ориентируясь на это свойство, строим модель программы, которая отражает все, что важно с точки зрения нашего свойства, а все остальное игнорирует. Модель может быть в разных формах, на практике чаще всего используют Spin, который тут уже упоминали, и описывают поведение программы на языке Promela. Потом по этому описанию строится структура Крипке: набор логических переменных, набор состояний, о каждом из которых известно, истинна или ложна в нем каждая переменная, и набор переходов между состояниями. Свойство, которое хочется проверять, записываем формально в какой-нибудь темпоральной логике (автоматный подход используется обычно для логики LTL). Берем отрицание полученной формулы. Дальше по структуре Крипке строим автомат Бюхи, он будет допускать возможные в системе (бесконечные) последовательности интерпретаций набора переменных. По LTL-формуле отрицания свойства тоже строим автомат Бюхи, он будет допускать такие последовательности интерпретаций переменных, которые нарушают интересующее нас свойство. Проверяем, что произведение этих автоматов допускает пустой язык. Это значит, что ни одна траектория в структуре Крипке не нарушает интересующего нас свойства. Если язык не пуст - это множество контрпримеров. Входными символами для автоматов являются интерпретации логических переменных структуры Крипке, которые обычно вычисляются на основе входов, выходов и иногда состояний анализируемой системы, так что можно потом по набору значений этих переменных определить, какие собственно входные воздействия имели место - каждый контрпример оказывается воспроизводимым багом.

Формально любой компьютер, выполняющий любую программу - это конечная система, но состояний там слишком много. Поэтому верифицируют (как и в случае с железом) не реальный код, а его модель. Хочется строить такие модели с как можно меньшими затратами человеческого труда, но здесь, мне кажется, еще работать и работать. До промышленного повседневного применения далеко, хотя есть интересные результаты (Java PathFinder (http://babelfish.arc.nasa.gov/trac/jpf), например).

[ivan-gandhi.livejournal.com]

Огромное спасибо! Узнал много новых слов и понятий.