City: Test Saint Petersburg Novosibirsk Kazan Language: Русский English

Введение в практическую верификацию. Система верификации SPIN (И.В.Шошмина, А.Б.Беляев)
Verification of the parallel and distributed systems

What: Lecture
When: Sunday, 18 March 2012, 13:00–14:35
Where: ПОМИ РАН
Slides: modelchecking_lecture_180312.pdf

Description

Доклад посвящен изложению методики использования программного средства 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, описывающих требования к программной системе.

Video