For example,Бобцов

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SPIN VERIFIER

Annotation

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

Articles in current issue