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

[juan_gandhi]

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

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

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

Comments

[panchul.livejournal.com]

А что, формальная верификация софтверных программ имеет реальное применение? В какой области? Я знаком только с формальной верификацией хардвера (поверхностно), и с динамической верификацией хардвера (coverage-driven constraint-random verification, SystemVerilog/VMM).

[ivan-gandhi.livejournal.com]

Это мой следующий вопрос: а что, собственно, это за штука такая, верификация программ? Верификация хардвера, для меня по крайней мере, имеет какой-то смысл, потому что хардвер конечен.

[panchul.livejournal.com]

Хардвер не совсем конечен. Хотя пространство состояний принципиально меньше, чем у софтвера, перебрать все пространство состояний и переходов даже простого устройства нереально. Именно для этого изобретены методологии с комбинацией динамической симуляции, формальной верификации, coverage и constraint random. Кроме этого в хардвере везде параллельность, что усложняет дело.

То, что верификация хардвера существует (как распостраненное занятие), а верификация софтвера - нет, объясняется не только "конечностью" хардвера, но и более высокими требованиями к качеству, чем у софтвера (после отправления дизайна на фабрику его не поменяешь (за исключением FPGA)). Верификация софтвера (I guess) наверное имеет практический смысл только для RTOS, которые маленькие, сильно параллельные, и имеют четко определенные абстракции (threads, mailbox, semaphore) и т.д.

[vit-r.livejournal.com]

Грубо говоря, по стандартам весь mission critical софт должен верифицироваться. В большинстве случаев, правда, это некий ручной процесс, близкое знакомство с которым лишает всяческих светлых иллюзий.

[99f.livejournal.com]

А вы пишете бесконечные программы? :-)

[ivan-gandhi.livejournal.com]

Можете поискать мою имплементацию аксиоматики Цермело-Френкеля. На джаве.

[panchul.livejournal.com]

По ссылке написано в основном про хардвер (combinational circuits, digital circuits with internal memory) и специальные случаи софтвера (cryptographic protocols, ..., and software expressed as source code.) Программные продукты для верификации хардвера на рынке существуют (например программы, которые доказывают те или иные свойства для RTL (register-transfer-level) дизайнов на Verilog, или которые определяют эквивалентность двух дизайнов, или верификация с помощью симуляции с хитрыми методами генерации случайных транзакций, подсчета покрытия и state space exploration. См. http://pikibook.com/electrical-engineering/digital-electronics/verilog-hdl/advanced-verification-techniques-summary

А вот программные продукты для верификации софтвера я не знаю, поэтому и спрашиваю. Я предполагаю, что они должны существовать для RTOS, которые маленькие, сильно параллельные, и имеют четко определенные абстракции (threads, mailbox, semaphore) и т.д. Но тогда встает вопрос - что для таких программ верификации является входным языком, который они парсируют? С/C++/Java? Эти языки труднее верифицировать, чем RTL-подмножество верилога ИМХО, ибо в них главную роль играют всякие динамические структуры (деревья с поинтерами), семантика которые на уровне языка не особенно видна (в то время как из кода на верилоге можно извлечь state machine).

[ivan-gandhi.livejournal.com]

Второй линк особенно прикольный. Сейчас, 14 лет спустя, было бы интересно вернуться к этому вопросу, действительно ли они что-то доказали в системе предотвращения наводнений в Голландии.

[ivan-gandhi.livejournal.com]

Вот и у меня такое же впечатление. :)

[vit-r.livejournal.com]

"Нет такой буквы в этом слове."

Практически, задача у верификации - доказать, что система не выдаст ошибочного значения. Правда, самая надёжная система - та, которая выключена. Но это тоже удовлетворяет условию задачи, хоть мало кто об этом любит говорить.

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

[vit-r.livejournal.com]

и выдаст правильное значение

Ну я ж русским языком пишу "практически"

В большинстве случаев она выдаёт правильное значение. В остальных - падает кверху лапками и производит перезапуск. Если может.

[mr-aleph.livejournal.com]

м, непонятно что значит верифицировать программу конечным автоматом.

[ivan-gandhi.livejournal.com]

Мне тоже, на самом деле.

[dtim.livejournal.com]

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

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

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

[huzhepidarasa.livejournal.com]

Хм. Вот есть программа
ispal x = x == reverse x
Можно ли верифицировать ее правильность конечным автоматом? Это же практически определение палиндрома, доказывать нечего. Может ли конечный автомат проверить, правильно ли записано определение? Хрен его знает, почему бы и нет? Во всяком случае, к какому классу относится язык, принимаемый программой, здесь вроде бы не играет роли. Нам больше интересен язык, на котором она написана.

[ivan-gandhi.livejournal.com]

Да. Хороший вопрос. Можно?

[huzhepidarasa.livejournal.com]

Да вот непонятно. С одной стороны вроде нельзя, надо хотя бы уметь имена переменных запоминать и потом сравнивать. С другой стороны, это тривиальная надстройка над конечным автоматом. Может, можно препроцессинг какой запустить и избавиться от таких переменных, а потом уже верифицировать. Содержательная часть — это доказательство некоторого утверждения о программе. Доказательства каких-то тривиальных утверждений можно породить конечным автоматом. Может быть, можно придумать язык, на котором легко писать так, чтобы большинство интересных нам утверждений были в нужном смысле тривиальными (типа «определение записано правильно»). Я не знаю.

[99f.livejournal.com]

Всякая программа на С имеет не более 2^{sizeof(void*)*CHAR_BIT} состояний (упражнение: обобщить последнее утверждение на случай программ работающих с файлами) и следовательно поведение всех программ в данной реализации стандарта может быть смоделировано и следовательно верифицировано неким конечным автоматом. Всякая программа на Java (ML, ...) может быть оттранслирована в программу на С, следовательно...

[ivan-gandhi.livejournal.com]

Вы и к стековой машине, к примеру, то же самое рассуждение примените?

[99f.livejournal.com]

Не понял что и как применить. Просто C как он описан в стандарте вопреки распространенному мнению не Turing complete. Программы на C можно верифицировать конечным автоматом. Можно разумеется и стековым. То же самое рассуждение применимо к более широкому классу языков.

Верификация программного обсепечения, неизвестная panchul, применяется военными и людьми занимающимися real-time. Есть периодическая конференция про это с proceedings на много сотен страниц. Spin и promela которые наверху упоминались вещи достаточно старые, они скорее про верификацию алгоритмов. Сейчас люди умеют верифицировать pointer arithmetics в многопоточных приложениях (Smallfoot, separation logic).