Verification of the formal requirements for the system behavior based on automaton objects

Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A. Verification of the formal requirements for the system behavior based on automaton objects. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2025, vol. 25, no. 2, pp. 328–338. doi: 10.17586/2226-1494-2025-25-2-328-338

The paper studies the problems of automatic verification of the behavior of a reactive system in accordance with formalized requirements, i.e., automatic verification. The reactive system is described by interconnected automaton objects. Formalized requirements are written as conditioned regular expressions. In this case mathematically reliable verification of the system is possible. The proposed solution is based on the use of the CIAO (Cooperative Interaction of Automaton Objects) language to specify the interaction of automaton objects. This paper considers the third version of the language, CIAO v.3, which defines the means of describing automaton classes, the means of instantiating automaton objects, and linking these objects to the system using a link diagram. The requirements to be verified are specified using the so-called conditioned regular expressions constructed over a set of elementary actions and conditions defined in the system. A software tool has been developed that, using a link diagram, builds a semantic graph, i.e., a directed graph, where all paths from the initial nodes represent the execution protocols of the automata-based program, thereby specifying the semantics of the reactive system. Then, it is checked whether the automata-based program complies with the requirement defined by the conditioned regular expression. If a discrepancy is detected, the tool shows the place where the semantic graph exactly does not comply with the requirement. Algorithms have been developed that allow automatic verification of reactive systems with respect to the formalized requirements of a certain class. An example of a program is given that demonstrates elevator control in the CIAO v.3 language, and the constructed reactive system is verified for compliance with formally specified requirements. The purpose of the article is to demonstrate software implementation of the tool for automatic verification of a program in the CIAO v.3 language.

1. Kulyamin V.V. Software Verification Methods. Moscow, ISP RAS, 2008, 111 p. (in Russian)

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

3. Lavrov S.S. Programming. Mathematical Foundations, Tools, Theory. St. Petersburg, BHV Petersburg Publ., 2001, 320 p. (in Russian)

4. Dijkstra E.W. A Discipline of Programming. Prentice Hall, 1976, 217 p.

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

6. Vinogradov R.A., Kuz'min E.V., Sokolov V.A. Verification of automata programs using CPN/Tools. Modelirovanie i analiz informacionnyh sistem, 2006, vol. 13, no. 2, pp. 4–15. (in Russian)

7. Shalyto A. Automata-based programming paradigm. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2008, vol. 53, pp. 3–23. (in Russian)

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

9. Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 1. Information and Control Systems, 2009, no. 6 (43), pp. 34–40. (in Russian)

10. Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 2. Information and Control Systems, 2010, no. 2 (45), pp. 31–37. (in Russian)

11. Novikov F.A., Tikhonova U.N. An Automata Based Method for Domain Specific Languages Definition. Part 3. Information and Control Systems, 2010, no. 3 (46), pp. 29–37. (in Russian)

12. Novikov F., Fedorchenko L., Vorobiev V., Fatkieva R., Levonevskiy D. Attribute-based approach of defining the secure behavior of automata objects. Proc. of the 10^th International Conference on Security of Information and Networks (SIN'17), 2017, pp. 67–72. https://doi.org/10.1145/3136825.3136887

13. Novikov F.A., Afanasyeva I.V. Cooperative interaction of automata objects. Information and control systems, 2016, no. 6 (85), pp. 50–64. (in Russian). https://doi.org/10.15217/issn1684-8853.2016.6.50

14. Afanasieva I.V. Data acquisition and control system for high-performance large-area CCD Systems. Astrophysical Bulletin, 2015, vol. 70, no. 2, pp. 232–237. https://doi.org/10.1134/S1990341315020108

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

16. Afanasyeva I.V., Novikov F.A., Fedorchenko L.N. Methodology for constructing event-driven software systems using the CIAO specification language. SPIIRAS Proceedings, 2020, vol. 19, no. 3, pp. 481–514. (in Russian). https://doi.org/10.15622/sp.2020.19.3.1

17. 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. https://doi.org/10.17586/2226-1494-2023-23-4-750-756

18. Novikov F.A., Afanasyeva I.V., Fedorchenko L.N., Kharisova T.A. Application of conditional regular expressions in problems of verification of control automata programs. 14th All-Russian conference on control problems. Collection of Scientific Papers. Moscow, IPU RAS, 2024, pp. 2651–2655. (in Russian)

19. Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A. Specification language for automatаbased objects cooperation. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2024, vol. 24, no. 6, pp. 1035–1043. https://doi.org/10.17586/2226-1494-2024-24-6-1035-1043

20. Novikov F.A., Afanasyeva I.V., Fedorchenko L.N., Kharisova T.A. Application of Conditional Regular Expressions in Verification Problems of Control Automata Programs. Proc. of Materials of the All-Russian Scientific Conference “PhysMech Science Week”, St. Petersburg, POLYTECH-PRESS, 2024, pp. 167–170. (in Russian)

21. Novikov F.A., Ivanov D.Iu. UML Modeling. Theory, Practice, Video Course. St. Petersburg, Professional’naja literature Publ., 2010, 640 p. (in Russian)

22. Shalyto A.A. Switch-Technology. Algorithmization and Programming of the Logical Control Problems. St. Petersburg, Nauka Publ., 1998, 617 p. (in Russian)

23. Velder S.E., Shalyto A.A. Methods of verification of models of automata-based programs. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2008, vol. 53, pp. 123–137. (in Russian)

24. Velder S.E., Lukin M.A., Shalyto A.A., Iaminov B.R. Verification of Automata-Based Programs. St. Petersburg, Nauka Publ., 2011, 244 p. (in Russian)

25. Kuzmin E.V., Sokolov V.A. Modeling, specification, and verification of automaton programs. Programming and Computer Software, 2008, vol. 34, no. 1, pp. 27–43. https://doi.org/10.1134/s0361768808010040

26. Gamma E., Helm R., Johnson R., Vlissides J. Design Patterns: Elements of Reusable Object-Oriented Software. Pearson Education, 1994, 416 p.

27. Gerasimov A.Y. Directed dynamic symbolic execution for static analysis warnings confirmation. Programming and Computer Software, 2018, vol. 44, no. 5, pp. 316–323. https://doi.org/10.1134/S036176881805002X

28. Friedl J.E.F. Mastering Regular Expressions: Understand Your Data and Be More. O'Reilly Media, Inc., 2006, 544 p.

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

 

 

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