ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN

Шалыто Анатолий Абрамович, Лукин Михаил Андреевич

2008 , ТОМ 08, НОМЕР 8 ( апрель )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Меню

Публикации

Главный редактор

НИКИФОРОВ
Владимир Олегович
д.т.н., профессор

Партнеры

УДК 004.4’242

ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN

Шалыто А.А., Лукин М.А.

Аннотация

Рассматривается способ использования верификатора SPIN для верификации автоматных программ. При использовании этого верификатора модель описывается на языке Promela, а требования – на языке LTL. В работе предлагается метод автоматизированного преобразования автоматных программ в модели на языке Promela. Для преобразования формулы на языке LTL в вид, пригодный для использования верификатором, разработано специальное программное средство. Использование предлагаемого метода иллюстрируется на примере верификации модели банкомата.

Ключевые слова:

верификация программ, верификация на моделях, автоматное программирование, верификатор SPIN

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License