Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:
Номер:8 (53)
Скачать PDF0 Кбайт
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.