Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets
Uniform systems of communicating extended finite automata are considered in the paper. These automata systems are useful for initial specification of telecommunication systems such as ring protocols and telephone networks. The goal of our paper is to represent an ASV tool (Automata Systems Verifier)...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2011-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1105 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849338692513038336 |
|---|---|
| author | D. M. Beloglazov M. Yu. Mashukov V. A. Nepomniaschy |
| author_facet | D. M. Beloglazov M. Yu. Mashukov V. A. Nepomniaschy |
| author_sort | D. M. Beloglazov |
| collection | DOAJ |
| description | Uniform systems of communicating extended finite automata are considered in the paper. These automata systems are useful for initial specification of telecommunication systems such as ring protocols and telephone networks. The goal of our paper is to represent an ASV tool (Automata Systems Verifier) intended for analysis and verification of the automata specifications. The ASV tool is based on the algorithm of translation of these automata systems into coloured Petri nets (CPN). This algorithm has been represented and justified in [4]. The ASV tool uses CPN Tools [10] for analysis of the net models and Petri Net Verifier [12] for their verification by the model checking method with respect to properties expressed in mu-calculus. Application of the ASV tool to ring protocol verification and investigation of feature interactions in telephone networks is described. |
| format | Article |
| id | doaj-art-33f9be39c5264836af31c1c2efd5c8ff |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2011-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-33f9be39c5264836af31c1c2efd5c8ff2025-08-20T03:44:19ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172011-12-01184144156846Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri NetsD. M. Beloglazov0M. Yu. Mashukov1V. A. Nepomniaschy2Институт систем информатики им. А.П. Ершова СО РАНИнститут систем информатики им. А.П. Ершова СО РАНИнститут систем информатики им. А.П. Ершова СО РАНUniform systems of communicating extended finite automata are considered in the paper. These automata systems are useful for initial specification of telecommunication systems such as ring protocols and telephone networks. The goal of our paper is to represent an ASV tool (Automata Systems Verifier) intended for analysis and verification of the automata specifications. The ASV tool is based on the algorithm of translation of these automata systems into coloured Petri nets (CPN). This algorithm has been represented and justified in [4]. The ASV tool uses CPN Tools [10] for analysis of the net models and Petri Net Verifier [12] for their verification by the model checking method with respect to properties expressed in mu-calculus. Application of the ASV tool to ring protocol verification and investigation of feature interactions in telephone networks is described.https://www.mais-journal.ru/jour/article/view/1105telecommunication systemsextended finite automatacoloured petri netsring protocolsfeature interactionstelephone networksverificationmodel checking method |
| spellingShingle | D. M. Beloglazov M. Yu. Mashukov V. A. Nepomniaschy Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets Моделирование и анализ информационных систем telecommunication systems extended finite automata coloured petri nets ring protocols feature interactions telephone networks verification model checking method |
| title | Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets |
| title_full | Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets |
| title_fullStr | Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets |
| title_full_unstemmed | Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets |
| title_short | Verification of Telecommunication Systems Specified by Communicating Finite Automata with the Help of Coloured Petri Nets |
| title_sort | verification of telecommunication systems specified by communicating finite automata with the help of coloured petri nets |
| topic | telecommunication systems extended finite automata coloured petri nets ring protocols feature interactions telephone networks verification model checking method |
| url | https://www.mais-journal.ru/jour/article/view/1105 |
| work_keys_str_mv | AT dmbeloglazov verificationoftelecommunicationsystemsspecifiedbycommunicatingfiniteautomatawiththehelpofcolouredpetrinets AT myumashukov verificationoftelecommunicationsystemsspecifiedbycommunicatingfiniteautomatawiththehelpofcolouredpetrinets AT vanepomniaschy verificationoftelecommunicationsystemsspecifiedbycommunicatingfiniteautomatawiththehelpofcolouredpetrinets |