пятница, 30 марта 2012 г.

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

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

Курс лекций: Верификация параллельных и распределенных программных систем

Предмет семинара: Computer Science

Аудитория курса: Computer Science клуб при ПОМИ РАН

Лектор лекции: Юрий Карпов, Ирина Шошмина

Тип лекции: Спецкурсы

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

Описание курса: Мини-курс посвящён изложению интересных новых результатов теоретической информатики, имеющих важное применение в верификации дискретных систем.