Верификация параллельных и распределенных программных систем. Лекция 2

Доклад посвящен изложению методики использования программного средства Spin с входным языком Promela, которое широко применяется для верификации протоколов, параллельных программ и широкого класса дискретных систем. Пакет Spin – свободно распространяемое программное средство для формальной верификации систем. Spin разработан в Исследовательском Центре Bell Labs Джерардом Холзманном (Jerard Holzmann) для проверки компьютерных протоколов. Ежегодно проводятся конференции пользователей этого пакета, в литературе широко обсуждаются многочисленные примеры применения Spin для верификации сложных систем, в том числе бортовых программ, разрабатываемых NASA.

Spin осуществляет проверку не программ, а моделей программ, построенных на С-подобном входном языке пакета Spin, названном автором Promela – Protocol Meta Language. В свою очередь, аббревиатура Spin расшифровывается как Simple Promela Interpreter – простой интерпретатор программ на языке Promela. Конструкции языка Promela просты, они имеют ясную и четкую семантику, позволяющую перевести (оттранслировать) любую программу на этом языке в систему переходов, которая далее анализируется. Программы на языке Promela переводятся в Spin’е в структуру Крипке, и затем на ней проверяется выполнение заданных формул темпоральной логики линейного времени LTL, описывающих требования к программной системе.

Страница лекции на сайте Computer Science клуба