<div>
	Verification of event-driven software systems using the specification language of cooperating automata objects</div>

Afanasieva Irina V. , Novikov Fedor A., Fedorchenko Ludmila N.

2023 , VOLUME 23, NUMBER 4 ( july-august )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

doi: 10.17586/2226-1494-2023-23-4-750-756

Verification of event-driven software systems using the specification language of cooperating automata objects

I. V. Afanasieva, F. A. Novikov, L. N. Fedorchenko

Read the full article

Article in English

For citation:

Afanasieva I.V., Novikov F.A., Fedorchenko L.N. Verification of event-driven software systems using the specification language of cooperating automata objects. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2023, vol. 23, no. 4, pp. 750–756. doi: 10.17586/2226-1494-2023-23-4-750-756

Abstract

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.

Keywords: verification, event-driven programs, critical system development, regular expressions, elevator control system

Acknowledgements. The work of Irina Afanasieva was carried out within the framework of the SAO RAS State Assignment approved by the Ministry of Science and Higher Education of the Russian Federation no. 121092300060-6.

References

Harel D., Pnueli D. On the development of reactive systems. Logics and Models of Concurrent Systems. Berlin, Heidelberg, Springer, 1985, pp. 477–498. https://doi.org/10.1007/978-3-642-82453-1_17
Karpov Iu.G. Model Checking. Verification of Parallel and Distributed Software Systems. St. Petersburg, BHV-Petersburg Publ., 2010, 560 p. (in Russian)
Sommerville I. Software Engineering. 10^th ed.Boston, Pearson, 2020.
Hinchey M., Coyle L. Evolving critical systems: a research agenda for computer-based systems. Proc. of the 17^th IEEE International Conference and Workshops on Engineering of Computer Based Systems, 2010, pp. 430–435. https://doi.org/10.1109/ECBS.2010.56
Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Automata-Based Program Verification. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)
Fedorchenko L., Baranov S. Equivalent transformations and regularization in context-free grammars. Cybernetics and Information Technologies,2015, vol. 14, no. 4, pp. 29–44. https://doi.org/10.1515/cait-2014-0003
Novikov F.A., Afanasieva I.V. Cooperative interaction of automata objects. Information and Control Systems, 2016, no. 6, pp. 50–64. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.6.50
Afanasieva I., Novikov F., Fedorchenko L. Methodology for development of event-driven software systems using ciao specification language. SPIIRAS Proceedings, 2020, no. 19, no. 3, pp. 481–514. (in Russian). https://doi.org/10.15622/sp.2020.19.3.1
Aho A.V., Lam M.S., Sethi R., Ullman J.D.Compilers: Principles, Techniques, and Tools. 2^nd ed.Boston, Pearson/Addison-Wesley, 2007, 1009 p.
Afanasieva I.V., Novikov F.A. Software architecture for optical detector systems. Information and Control Systems, 2016, no. 3, pp. 51–63. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.3.51
Novikov F.A., Ivanov D.Iu. UML Modeling. Theory, Practice, Video Course. St. Petersburg, Professional'naja literature Publ., 2010, 649 p.
Knuth D.E.The Art of Computer Programming, V. 1. Fundamental Algorithms. 3^rd ed.Addison-Wesley Professional, 1997, 672 p.
Polikarpova N.I., Shalyto A.A. Automata-Based Programming. St. Petersburg, Piter Publ., 2011, 176 p. (in Russian)
Fan W., Li J., Ma S., Tang N., Wu Y., Wu Y. Graph pattern matching: From intractable to polynomial time. Proceedings of the VLDB Endowment, 2010, vol. 3, no. 1–2, pp. 264–275. https://doi.org/10.14778/1920841.1920878
Avdoshin S.M., Nabebin A.A. Discrete Mathematics. Formal Logic Systems and Languages. Moscow, DMK Press Publ., 2018, 390 p. (in Russian)
Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verification of internet protocol properties using cooperating automaton objects. Proc. of the 12^th International Conference on Security of Information and Networks (SIN'19), 2019, pp. 1–4. https://doi.org/10.1145/3357613.3357639
Dijkstra E.W. A Discipline of Programming. 3^rd ed. Englewood Cliffs, N.J., Prentice Hall, 1976, 217 p.
Shalyto A.A. Validation of state machine specifications. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2023, vol. 23, no. 2, pp. 436–438. (in Russian). https://doi.org/10.17586/2226-1494-2023-23-2-436-438

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License