Development and Automatic Verification of Parallel Automatа-Based Software
Keywords:
Automaton, Parallel Automatа-Based Software, Verification, Model Checking, Linear Temporal Logics, SpinAbstract
There has been considered a complex approach to development and verification of parallel automata-based programs where hierarchical automata can be implemented in separate flows and interact. The interactive approach to verification of parallel automatabased programs using Spin has been proposed. It includes robotized model construction in Promela, LTL-formula conversion into Spin format and construction of a counter-example in automata terms.
Published
2013-10-18
How to Cite
Lukin, M., & Shalyto, A. (2013). Development and Automatic Verification of Parallel Automatа-Based Software. Information and Control Systems, (5), 3–50. Retrieved from http://ia.spcras.ru/index.php/ius/article/view/13674
Issue
Section
Hardware and software resources