Menu
Publications
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.
Partners
doi: 10.17586/2226-1494-2025-25-2-328-338
Verification of the formal requirements for the system behavior based on automaton objects
Read the full article

Article in English
For citation:
Abstract
For citation:
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
Abstract
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.
Keywords: automatic verification, conditioned regular expressions, behavior model, automata-based programming, state transition
graph, UML, state machine diagram, concurrent behavior, software architecture, reactive system
References
References
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 10th 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 12th 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