VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER

Shalyto Anatoly A., Michael Lukin

2008 , VOLUME 08, NUMBER 8 ( April )

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

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER

A. A. Shalyto, M. Lukin

Read the full article

Abstract

A way to use SPIN verifier for the verification of automata-based programs is proposed. When using this verifier model is described with Promela language and requirements are specified with LTL language. A method of automated automata-based program to Promela model transformation is proposed. For LTL-formulas

transformation a special program was developed. Usage of this methods is illustrated on the example of cashmachine model verification.

Keywords: program verification, model checking, automata-based programming, SPIN verifier

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