УДК 004.4’242

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

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



Аннотация

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


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

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

Информация 2001-2017 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика