Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N2 2024 year

DOI: 10.17587/prin.15.73-86
Automata-based Software Engineering for Control System Design and Verification
V. I. Shelekhov, Head of Laboratory, vshel@iis.nsk.su, E. G. Tumurov, Research Assistant, erdemus@gmail.com, A. P. Ershov Institute of Informatics Systems, Novosibirsk, 630090, Russian Federation
Corresponding author: Vlaimir I. Shelekhov, Head of Laboratory, A. P. Ershov Institute of Informatics Systems, Novosibirsk, 630090, Russian Federation, E-mail: vshel@iis.nsk.su
Received on October 31, 2023
Accepted on November 22, 2023

The automata composition is defined as the basic language construct of automata programming. Incorporating automata composition into an arbitrary programming language allows the development of automata programs in that language. Methods for specification and verification of reactive systems are defined in detail. All kinds of correctness formulas for a reactive system with respect to its specification are defined. In addition, correctness formulas for verification using the full invariant of the reactive system are developed. The Event-B manual begins with a brilliant illustration of the basic Event-B methods using the example of a car traffic control problem on a narrow bridge. However, the latter refinement in this illustration generates a complex cumbersome program. A simpler and shorter solution to this problem was presented in our work [7] using automata programming approach. Our solution was not easy because 4 non-trivial bugs were found by verification in Event-B. This paper describes our third attempt to construct a short simple automata program to solve this problem. Verification of the automata program in Event-B and Why3 systems was carried out. No errors were found. For verification, a reactive system model is built on Why3, which is simpler and more universal than the why3-do model.

Keywords: automata-based engineering, Event-B, Why3, why3-do, refinement, requirements, program transformation, deductive verification, functional programming
pp. 73–86
For citation:
Shelekhov V. I., Tumurov E. G. Automata-based Software Engineering for Control System Design and Verification, Programmnaya Ingeneria, 2024, vol. 15, no. 2, pp. 73—86. DOI: 10.17587/prin.15.73-86. (in Russian).
References:
    • Abrial J.-R. Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010, 586 p.
    • Kharnaukhov N., Perchine D., Shelekhov V. The predicate programming language P, Novosibirsk, ISI SB RAN, 2018, 45 p. (in Russian).
    • Shelekhov V. I. Automata-based software engineering: the language and development methods, Programmnaya Ingeneria, 2014, no. 4, pp. 3—15. DOI: 10.17587/prin.8.99-111 (in Russian).
    • Tumurov E. G., Shelekhov V. I. Applying Automata-based Software Engineering for the Lift Control Program, Programmnaya Ingeneria, 2017, vol. 8, no. 4, pp. 99—111 (in Russian).
    • Shelekhov V. I. Automata-based programming on the base of requirements specification, Sistemnaya Informatika, Novosibirsk, ISI SB RAN, 2014, no. 4, pр. 1—29. DOI: 10.31144/si.2307-6410.2014.n4.p1-29 (in Russian).
    • Shelekhov V. I. Automata-based Program Optimization by Applying Requirement Transformations. Programmnaya Ingeneria, 2015, no. 11, pp. 3—13 (in Russian).
    • Shelekhov V. I. Automata-based Software Engineering with Event-B, Programmnaya Ingeneria, 2022, vol. 13, no. 4, pp. 155—167. DOI: 10.17587/prin.13.155-167 (in Russian).
    • Shelekhov V. I. Program Classification in Software Engineering, Programmnaya Ingeneria, 2016, vol. 7, no. 12, pp. 531—538. DOI: 10.17587/prin.7.531-538 (in Russian).
    • Shelekhov V. I. Development of a program for building a suffix tree in the predicate software engineering, Preprint, no. 115, Novosibirsk, ISI SB RAN, 2004, 52 p. (in Russian).
    • Shelekhov V. I. Development and verification of the heapsort algorithms in predicate software engineering, Preprint no. 164, Novosibirsk, ISI SB RAN, 2012, 30 p. (in Russian).
    • Polykarpova N. I., Shalyto А. А. Automata-base programming, Second edition, St. Petersburg, Piter, 2020, 176 p. (in Russian).
    • Systems and software engineering — Life cycle processes — Requirements engineering. ISO/IEC/IEEE 29148, 2011, 95 p.
    • Hoare С. A. R. An axiomatic basis for computer programming, Communications of the ACM, 1969, vol. 12, issue 10, pp. 576—585. DOI: 10.1145/363235.363259.
    • Floyd R. W. Assigning meanings to programs. Proceedings Symposium in Applied Mathematics, Mathematical Aspects of ComputerScience. AMS, 1967, pp. 19—32.
    • Why 3. Where Programs Meet Provers, available at: http:// why3.lri.fr (date of access 30.10.2023).
    • Hoang T. S., Dghaym D., Snook C., Butler M. A Composition Mechanism for Refinement-Based Methods, 22nd International Conference on Engineering of Complex Computer Systems (ICECCS), 2017, pp. 100—109. DOI: 10.1109/ICECCS.2017.27.
    • Shelekhov V. I., Tumurov E. G. Development and verification of automata programs for control systems, Nauka i Texnologiya v Sibiri, 2023, vol. 10, pp. 100—106.
    • Rodin User's Handbook. Version 2.8. / Ed. M. Jastram, Deploy Project, 2014, 184 p.
    • Owre S., Rushby J. M., Shankar N. PVS: Specification and Verification System, CADE-11: Automated Deduction, LNCS vol. 607, 1992, pp. 748—752. DOI: 10.1007/3-540-55602-8_217.
    • The Coq Proof Assistant, available at: http://coq.inria.fr (date of access 30.10.2023).
    • Shelekhov V. I. Deductive verification of a simple mutual exclusion protocol, 18th conf. Raspredelenny'e informacionno-vy'chislitel'ny'e resursy (DICR-2022), Novosibirsk, 2022, pp. 229—235 (in Russian).
    • Lourenco С. B., Pinto J. S. Why3-do: The Way of Harmonious Distributed System Proofs, Programming Languages and Systems, ESOP 2022, LNCS vol. 13240, 2022, pp. 114—142. DOI: 10.1007/978-3-030-99336-8_5.
    • Milner R. Communication and Concurrency, International Series in Computer Science. Prentice Hall, 1989, 272 p.
    • Hoare С. A. R. Communicating Sequential Processes, Prentice Hall International, 1985, 260 p.
    • Larson J. Erlang for concurrent programming, ACM Queue, 2008, no. 5, pp. 18—23.
    • Silva L., Oliveira M. Automatic Generation of Verified Concurrent Hardware Using VHDL, Formal Methods: Foundations and Applications, SBMF 2022, LNCS vol. 13768, 2022, pp. 55—72. DOI: 10.1007/978-3-031-22476-8_4.
    • Jesus J., Sampaio A. Compositional Verification of Simulink Block Diagrams Using tock-CSP and CSP-Prover, Formal Methods: Foundations and Applications, SBMF 2022, LNCS vol. 13768, 2022, pp. 91—108. DOI: 10.1007/978-3-031-22476-8_6.
    • Riviere P., Singh N. K., Ait-Ameur Y. Reflexive Event-B: Semantics and Correctness The EB4EB framework, IEEE Transactions on Reliability, 2022, pp. 1—16. DOI: 10.1109/TR.2022.3219649.
    • Riviere P., Singh N. K., Ait-Ameur Y. EB4EB: A Framework for Reflexive Event-B, 26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), 2022, pp. 71—80. DOI: 10.1109/ICECCS54210.2022.00017.
    • Riviere P., Singh N. K., Ait-Ameur Y., Dupont G. Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework, NASA Formal Methods NFM 2023, LNCS vol. 13903, 2023, pp. 312—331. DOI: 10.1007/978-3-031-33170-1_19.
    • Riviere P., Singh N. K., Ait Ameur Y., Dupont G. Standalone Event-B models analysis relying on the EB4EB meta-theory, International Conference on Rigorous State Based Methods, ABZ 2023, LNCS vol. 14010, 2023, pp. 193—211. DOI: 10.1007/978-3-031-33163-3_15.