METHODS OF AUTOMATA-BASED PROGRAMS VERIFICATION

Sergey Velder, Shalyto Anatoly Abramovich

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

METHODS OF AUTOMATA-BASED PROGRAMS VERIFICATION

S. Velder, A. A. Shalyto

Read the full article

Abstract

This article discusses ways of converting automata-based programs to Kripke models, designed to check the properties related to the behavior of the system. These properties are described with temporal logic formulas. Several methods of such a transformation are proposed.

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

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