doi: 10.17586/2226-1494-2024-24-6-1035-1043


Specification language for automatа-based objects cooperation

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


Read the full article  ';
Article in English

For citation:
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. doi: 10.17586/2226-1494-2024-24-6-1035-1043


Abstract
Automata-based programming is a programming paradigm that has been successfully used in the development of reactive systems, distributed control systems, and various mission-critical applications where the ability to verify the compliance of a real system with its model given in the form of specifications is critical. The traditional testing of such systems can be difficult; thus, more advanced verification tools are required to increase confidence in the reliability of real systems. The previously proposed language for the specification of the Cooperative Interaction of Automata-based Objects (CIAO) was successfully used to develop several different reactive systems as a result of which a number of shortcomings were identified and eliminated in the new version of CIAO v.3. This new version of the language was developed for the automatic verification of automata-based programs according to the formal specifications of a certain class of real-time systems. Three innovations distinguish CIAO v.3 from previous versions. First, an explicit distinction between automata classes and automaton objects as instances of these classes. Second, we specify the binding of automaton objects through interfaces using a connection scheme. Third, we describe the semantics of the behavior of a system of interacting automaton objects using a semantic graph. This paper presents the main concepts of the new language version including the abstract syntax, operational semantics, and metamodel. The third version of the CIAO language naturally includes almost all the advantages of object-oriented programming into the paradigm of automata programming. The connection of automaton objects through the corresponding interfaces is arbitrarily reflected by the connection scheme. A semantic graph describing the semantics of the behavior of the automata-based program is used to implement automatic verification with respect to formal specifications.

Keywords: behavior model, automata-based programming, state transition graph, UML, state machine diagram, class diagram, concurrent behavior, software architecture, reactive system

References
  1. Shalyto A.A. Software implementation of the control automata. Sudostroitel’naja promyshlennost’. Serija «Avtomatika i telemehanika», 1991, vol. 13, pp. 41–42. (in Russian)
  2. Harel D. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 1987, vol. 8, no. 3, pp. 231–274. https://doi.org/10.1016/0167-6423(87)90035-9
  3. Harel D., Pnueli A. 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
  4. Harel D., Feldman Y.A. Algorithmics: The Spirit of Computing. London, Pearson Education, 2004, 513 p. https://doi.org/10.1007/978-3-642-27266-0
  5. Shalyto A.A. Switch-Technology. Algorithmization and Programming of the Logical Control Problems. St. Petersburg, Nauka Publ., 1998, 617 p. (in Russian)
  6. Polikarpova N.I., Shalyto A.A. Automata-Based Programming. St. Petersburg, Piter Publ., 2011, 176 p. (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. 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
  9. 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
  10. 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
  11. 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
  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., Ivanov D.Iu. UML Modeling. Theory, Practice, and Video Course. St. Petersburg, Professional’naja Literature Publ., 2010, 649 p. (in Russian).
  14. 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
  15. Rumbaugh J., Jacobson I., Booch G. The Unified Modeling Language Reference Manual. 2nd ed. Addison-Wesley Professional, 2010.
  16. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to Automata Theory, Languages, and Computation. 3rd ed. Boston, Addison-Wesley, 2006, 535 p.
  17. Meyer B. Object-Oriented Software Construction. 2nd ed. Prentice-Hall, 1997, 1254 p.
  18. Lavrov S.S. Programming. Mathematical Foundations, Instrumentation, Theory.St. Petersburg, BHV-Petersburg Publ., 2001, 320 p. (in Russian)
  19. Friedl J.E.F. Mastering Regular Expressions. 3rd ed. O’Reilly, 2006.
  20. Novikov F.A., Tikhonova U.N. An automata based method for domain specific languages definition. Part 3. Information and Control Systems, 2010, no. 3, pp. 29–37. (in Russian).
  21. 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
  22. Novikov F.A., Afanasieva I.V., Fedorchenko L.N., Kharisova T.A. Application of conditional regular expressions in the problems of verification of control automata programs. Proc. of the XIV All-Russian Conference on Management Problems (VSPU-2024), Moscow, V.A. Trapeznikov Institute of Control Sciences of Russian Academy of Sciences, 2024, pp. 2960–2964. (in Russian)
  23. Meyer B. Touch of Class: Learning to Program Well with Objects and Contracts. Berlin, Springer, 2009, 876 p. https://doi.org/10.1007/978-3-540-92145-5
  24. Weisfeld M. The Object-Oriented Thought Process. 5th ed. Addison-Wesley Professional, 2019.


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2025 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика