Operational semantics of annotated Reflex programs

I. S. Anureev

Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 475-487.

Résumé

Reflex is a process-oriented language that provides a design of easy-to-maintain control software for programmable logic controllers. The language has been successfully used in a several reliability critical control systems, e. g. control software for a silicon single crystal growth furnace and electronic equipment control system. Currently, the main goal of the Reflex language project is to develop formal verification methods for Reflex programs in order to guarantee increased reliability of the software created on its basis. The paper presents the formal operational semantics of Reflex programs extended by annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief overview of the Reflex language is given and a simple example of its use – a control program for a hand dryer – is provided. The concepts of environment and variables shared with the environment are defined that allows to disengage from specific input/output ports. Types of annotations that specify restrictions on the values of the variables at program launch, restrictions on the environment (in particular, on the control object), invariants of the control cycle, pre- and postconditions of external functions used in Reflex programs are defined. Annotated Reflex also uses standard annotations assume, assert and havoc. The operational semantics of the annotated Reflex programs uses the global clock as well as the local clocks of separate processes, the time of which is measured in the number of iterations of the control cycle, to simulate time constraints on the execution of processes at certain states. It stores a complete history of changes of the values of shared variables for a more precise description of the time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of process transition management from state to state and the interaction of processes with each other and with the environment. Extending the formal operational semantics of the Reflex language to annotations simplifies the proof of the correctness of the transformation approach to deductive verification of Reflex programs developed by the authors, transforming an annotated Reflex program to an annotated program in a very limited subset of the C language, by reducing a complex proof of preserving the truth of program requirements during the transformation to a simpler proof of equivalence of the original and the resulting annotated programs with respect to their operational semantics.

Détail

Keywords: operational semantics, Reflex language, control system, control software, programmable logic controller, annotated program.
Mots-clés : annotation

Bibliographie

[1] Programmable Controllers–Part 3: Programming Languages, International Standard IEC 61131-3, Second Edition, International Electrotechnical Commission, 2003-1

[2] Basile F., Chiacchio P., Gerbasio D., “On the Implementation of Industrial Automation Systems Based on PLC”, IEEE Transactions on Automation Science and Engineering, 10:4 (2012), 990–1003 | DOI

[3] Travis J., Kring J., LabVIEW for Everyone: Graphical Programming Made Easy and Fun, Third Edition, Prentice Hall PTR, Upper Saddle River, NJ, USA, 2006

[4] Zyubin V., “Using Process-Oriented Programming in LabVIEW”, Proceedings of the Second IASTED International Multi-Conference on "Automation, Control, and Information technology": Control, Diagnostics, and Automation, Novosibirsk, 2010, 35–41

[5] Buxton J. N., Randell B., Software Engineering Techniques, Report on a Conference Sponsored by the NATO Science Committee, NATO Science Committee, Brussels; Scientific Affairs Division, NATO, Rome, Italy, 1970

[6] Anureev I. S., Garanina N. O., Liakh T. V., Rozov A. S., Zyubin V. E., Gorlatch S., “Two-Step Deductive Verification of Control Software Using Reflex”, Preliminary Proceedings of A. P. Ershov Informatics Conference (PSI-19) (Novosibirsk, Russia, Akademgorodok, Russia, July 2-5, 2019), 17–30

[7] Anureev I. S., Garanina N. O., Liakh T. V., Rozov A. S., Schulte H., Zyubin V. E., “Towards Safe Cyber-Physical Systems: the Reflex Language and its Transformational Semantics”, 14th International Siberian Conference on Control and Communications (SIBCON) (Tomsk State University of Control Systems and Radioelectronics, Tomsk, April 18-20, 2019), 1–6

[8] Zyubin V. E., Liakh T. V., Rozov A. S., “Reflex Language: a Practical Notation for Cyber-Physical Systems”, System Informatics, 12 (2018), 85–104

[9] Norrish M., C Formalised in HOL, Ph.D. thesis, Technical Report, UCAM-CL-TR-453, University of Cambridge, 1998 | MR

[10] Gurevich Y., Huggins J., “The Semantics of the C Programming Language”, International Workshop on Computer Science Logic, Lecture Notes in Computer Science, 702, 1992, 274–308 | DOI

[11] Blazy S., Leroy X., “Mechanized Semantics for the Clight Subset of the C Language”, Journal of Automated Reasoning, 43:3 (2009), 263–288 | DOI | MR | Zbl

[12] Nepomniaschy V. A., Anureev I. S., Mikhailov I. N., Promsky A. V., “Towards Verification of C Programs. C-light Language and its Formal Semantics”, Programming and Computer Science, 28:6 (2002), 314–323 | DOI | Zbl

[13] Ellison C., Rosu G., “An Executable Formal Semantics of C with Applications”, Proc. of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, ACM SIGPLAN Notices, 47, no. 1, 2012, 533–544 | DOI