VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS
The paper deals with an interactive method of automatic verification for parallel automata-based programs. The hierarchical state machines can be implemented in different threads and can interact with each other. Verification is done by means of Spin tool and includes automatic Promela model const...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)
2014-01-01
|
| Series: | Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki |
| Subjects: | |
| Online Access: | http://ntv.ifmo.ru/file/article/8396.pdf |
| Summary: | The paper deals with an interactive method of automatic verification for parallel automata-based programs. The hierarchical
state machines can be implemented in different threads and can interact with each other. Verification is done by means of
Spin tool and includes automatic Promela model construction, conversion of LTL-formula to Spin format and counterexamples
in terms of automata. Interactive verification gives the possibility to decrease verification time and increase the maximum
size of verifiable programs. Considered method supports verification of the parallel system for hierarchical automata
that interact with each other through messages and shared variables. The feature of automaton model is that each state machine
is considered as a new data type and can have an arbitrary bounded number of instances. Each state machine in the
system can run a different state machine in a new thread or have nested state machine. This method was implemented in the
developed Stater tool. Stater shows correct operation for all test cases. |
|---|---|
| ISSN: | 2226-1494 2500-0373 |