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 |
| _version_ | 1818358952802385920 |
|---|---|
| author | M. A. Lukin |
| author_facet | M. A. Lukin |
| author_sort | M. A. Lukin |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-13T20:37:11Z |
| format | Article |
| id | doaj.art-614ca669842c440c87da71a0d204182d |
| institution | Directory Open Access Journal |
| issn | 2226-1494 2500-0373 |
| language | English |
| last_indexed | 2024-12-13T20:37:11Z |
| publishDate | 2014-01-01 |
| publisher | Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) |
| record_format | Article |
| series | Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki |
| spelling | doaj.art-614ca669842c440c87da71a0d204182d2022-12-21T23:32:16ZengSaint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki2226-14942500-03732014-01-011416066VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMSM. A. LukinThe 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.http://ntv.ifmo.ru/file/article/8396.pdfparallel automata-based programsverificationmodel checkinglinear temporal logicstate machinesSpin |
| spellingShingle | M. A. Lukin VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki parallel automata-based programs verification model checking linear temporal logic state machines Spin |
| title | VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS |
| title_full | VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS |
| title_fullStr | VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS |
| title_full_unstemmed | VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS |
| title_short | VERIFICATION OF PARALLEL AUTOMATA-BASED PROGRAMS |
| title_sort | verification of parallel automata based programs |
| topic | parallel automata-based programs verification model checking linear temporal logic state machines Spin |
| url | http://ntv.ifmo.ru/file/article/8396.pdf |
| work_keys_str_mv | AT malukin verificationofparallelautomatabasedprograms |