Verifcation of event-driven software systems using the specifcation language of cooperating automata objects

The CIAO (Cooperative Interaction Automata Objects) specifcation 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 (Unifed Modeling Language) with the possibility of cooperative interaction of several automata through strictly defned interfaces. The cooperative interaction of automatа objects is defned by a link scheme that defnes 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 fnal nodes defne sequences of interface method calls. Because the interfaces are strictly defned 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 defne 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 specifcation formalism to the class of regular languages and the programming language to a language with a simple and predefned structure. In many practical cases, this is suffcient for effective verifcation.

1. 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

2. Karpov Iu.G. Model Checking. Verifcation of Parallel and Distributed Software Systems. St. Petersburg, BHV-Petersburg Publ., 2010, 560 p. (in Russian)

3. Sommerville I. Software Engineering. 10th ed. Boston, Pearson, 2020.

4. Hinchey M., Coyle L. Evolving critical systems: a research agenda for computer-based systems. Proc. of the 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, 2010, pp. 430–435. https://doi.org/10.1109/ECBS.2010.56

5. Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Automata-Based Program Verifcation. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)

6. 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

7. 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

8. Afanasieva I., Novikov F., Fedorchenko L. Methodology for development of event-driven software systems using ciao specifcation language. SPIIRAS Proceedings, 2020, no. 19, no. 3, pp. 481–514. (in Russian). https://doi.org/10.15622/sp.2020.19.3.1

9. Aho A.V., Lam M.S., Sethi R., Ullman J.D. Compilers: Principles, Techniques, and Tools. 2nd ed. Boston, Pearson/Addison-Wesley, 2007, 1009 p.

10. 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

11. Novikov F.A., Ivanov D.Iu. UML Modeling. Theory, Practice, Video Course. St. Petersburg, Professional’naja literature Publ., 2010, 649 p.

12. Knuth D.E. The Art of Computer Programming, V. 1. Fundamental Algorithms. 3rd ed. Addison-Wesley Professional, 1997, 672 p.

13. Polikarpova N.I., Shalyto A.A. Automata-Based Programming. St. Petersburg, Piter Publ., 2011, 176 p. (in Russian)

14. 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

15. Avdoshin S.M., Nabebin A.A. Discrete Mathematics. Formal Logic Systems and Languages. Moscow, DMK Press Publ., 2018, 390 p. (in Russian)

16. Levonevskiy D., Novikov F., Fedorchenko L., Afanasieva I. Verifcation of internet protocol properties using cooperating automaton objects. Proc. of the 12th International Conference on Security of Information and Networks (SIN’19), 2019, pp. 1–4. https://doi.org/10.1145/3357613.3357639

17. Dijkstra E.W. A Discipline of Programming. 3rd ed. Englewood Cliffs, N.J., Prentice Hall, 1976, 217 p.

18. Shalyto A.A. Validation of state machine specifcations. Scientifc 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