Verification of event-driven software systems using the specification language of cooperating automata objects
The CIAO (Cooperative Interaction Automata Objects) specification language is intended to describe the behavior of distributed and parallel event-driven systems. This class of systems includes various software and hardware systems for control, monitoring, data collection, and processing. The ability...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)
2023-08-01
|
| Series: | Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki |
| Subjects: | |
| Online Access: | https://ntv.ifmo.ru/file/article/22199.pdf |
| _version_ | 1797740096165773312 |
|---|---|
| author | Irina V. Afanasieva Fedor A. Novikov Ludmila N. Fedorchenko |
| author_facet | Irina V. Afanasieva Fedor A. Novikov Ludmila N. Fedorchenko |
| author_sort | Irina V. Afanasieva |
| collection | DOAJ |
| description | The CIAO (Cooperative Interaction Automata Objects) specification language is intended to describe the behavior of distributed and parallel event-driven systems. This class of systems includes various software and hardware systems for control, monitoring, data collection, and processing. The ability to verify compliance with requirements is desirable competitive advantage for such systems. The CIAO language extends the concept of state machines of the UML (Unified Modeling Language) with the possibility of cooperative interaction of several automata through strictly defined interfaces. The cooperative interaction of automatа objects is defined by a link scheme that defines how the provided and required interfaces of different automatа objects are connected. Thus, the behavior of the system as a
whole could be described as a set of execution protocols, each of which is a sequence of interface calls, possibly with guard conditions. We represent a set of protocols using a semantic graph in which all possible paths from the initial nodes to the final nodes define sequences of interface method calls. Because the interfaces are strictly defined in advance by the connection scheme, it is possible to construct a semantic graph automatically according to a given system of
interacting automaton objects. To verify the system behavior, one only has to check if each path in the semantic graph does satisfy the requirements. System requirements are formally described using conditional regular expressions that define patterns of acceptable and forbidden behavior. This article proposes methods and algorithms that allow you to check the compliance of programs in the CIAO language with the requirements automatically and, thereby, check the semantics of the developed program. The proposed method narrows the specification formalism to the class of regular languages and the programming language to a language with a simple and predefined structure. In many practical cases, this is sufficient for effective verification. |
| first_indexed | 2024-03-12T14:07:37Z |
| format | Article |
| id | doaj.art-4d15bf0db4a84e0f8aa8bd180eabb380 |
| institution | Directory Open Access Journal |
| issn | 2226-1494 2500-0373 |
| language | English |
| last_indexed | 2024-03-12T14:07:37Z |
| publishDate | 2023-08-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-4d15bf0db4a84e0f8aa8bd180eabb3802023-08-21T11:43:02ZengSaint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University)Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki2226-14942500-03732023-08-0123475075610.17586/2226-1494-2023-23-4-750-756Verification of event-driven software systems using the specification language of cooperating automata objectsIrina V. Afanasieva0https://orcid.org/0000-0003-4225-4124Fedor A. Novikov1https://orcid.org/0000-0003-4450-0173Ludmila N. Fedorchenko2https://orcid.org/0000-0002-4008-9316PhD, Head of Laboratory, Special Astrophysical Observatory of the Russian Academy of Sciences (SAO RAS), Nizhny Arkhyz, 369167, Russian Federation, sc 57210431774D.Sc., Senior Researcher, Professor, Peter the Great St. Petersburg Polytechnic University (SPbPU), Saint Petersburg, 195251, Russian Federation; Professor, Alferov Academic University, Saint Peterburg, 194021, Russian Federation, sc 16441904500PhD, Senior Researcher, St. Petersburg Federal Research Center of the Russian Academy of Sciences, Saint Petersburg, 199178, Russian Federation, sc 36561350100The CIAO (Cooperative Interaction Automata Objects) specification language is intended to describe the behavior of distributed and parallel event-driven systems. This class of systems includes various software and hardware systems for control, monitoring, data collection, and processing. The ability to verify compliance with requirements is desirable competitive advantage for such systems. The CIAO language extends the concept of state machines of the UML (Unified Modeling Language) with the possibility of cooperative interaction of several automata through strictly defined interfaces. The cooperative interaction of automatа objects is defined by a link scheme that defines how the provided and required interfaces of different automatа objects are connected. Thus, the behavior of the system as a whole could be described as a set of execution protocols, each of which is a sequence of interface calls, possibly with guard conditions. We represent a set of protocols using a semantic graph in which all possible paths from the initial nodes to the final nodes define sequences of interface method calls. Because the interfaces are strictly defined in advance by the connection scheme, it is possible to construct a semantic graph automatically according to a given system of interacting automaton objects. To verify the system behavior, one only has to check if each path in the semantic graph does satisfy the requirements. System requirements are formally described using conditional regular expressions that define patterns of acceptable and forbidden behavior. This article proposes methods and algorithms that allow you to check the compliance of programs in the CIAO language with the requirements automatically and, thereby, check the semantics of the developed program. The proposed method narrows the specification formalism to the class of regular languages and the programming language to a language with a simple and predefined structure. In many practical cases, this is sufficient for effective verification.https://ntv.ifmo.ru/file/article/22199.pdfverificationevent-driven programscritical system developmentregular expressionselevator control system |
| spellingShingle | Irina V. Afanasieva Fedor A. Novikov Ludmila N. Fedorchenko Verification of event-driven software systems using the specification language of cooperating automata objects Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki verification event-driven programs critical system development regular expressions elevator control system |
| title | Verification of event-driven software systems using the specification language of cooperating automata objects |
| title_full | Verification of event-driven software systems using the specification language of cooperating automata objects |
| title_fullStr | Verification of event-driven software systems using the specification language of cooperating automata objects |
| title_full_unstemmed | Verification of event-driven software systems using the specification language of cooperating automata objects |
| title_short | Verification of event-driven software systems using the specification language of cooperating automata objects |
| title_sort | verification of event driven software systems using the specification language of cooperating automata objects |
| topic | verification event-driven programs critical system development regular expressions elevator control system |
| url | https://ntv.ifmo.ru/file/article/22199.pdf |
| work_keys_str_mv | AT irinavafanasieva verificationofeventdrivensoftwaresystemsusingthespecificationlanguageofcooperatingautomataobjects AT fedoranovikov verificationofeventdrivensoftwaresystemsusingthespecificationlanguageofcooperatingautomataobjects AT ludmilanfedorchenko verificationofeventdrivensoftwaresystemsusingthespecificationlanguageofcooperatingautomataobjects |