Operational Semantics of Annotated Reflex Programs

作     者：Anureev, I. S. 

作者机构：Russian Acad Sci Siberian Branch Ershov Inst Informat Syst Novosibirsk 630090 Russia Russian Acad Sci Siberian Branch Inst Automat & Electrometry Novosibirsk 630090 Russia 

出 版 物：《AUTOMATIC CONTROL AND COMPUTER SCIENCES》 (自动控制与计算机科学)

年 卷 期：2020年第54卷第7期

页      面：719-727页

核心收录：

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 0811[工学-控制科学与工程] 

基　　金：RFBR [17-07-01600] Russian Ministry of Education and Science [AAAA-A19-119120290056-0] 

主　　题：operational semantics Reflex language control system control software programmable logic controller annotation annotated program 

摘      要：Reflex is a process-oriented language for developing easy-to-maintain control software for programmable logic controllers. The language has been successfully used in several safety-critical control systems, e.g., in control systems of a silicon single crystal growing furnace and electronic equipment. 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 formal operational semantics of Reflex programs extended with annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief review 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, which make it possible to abstract from specific input/output ports. Types of annotations that specify constraints on the values of the variables at program start, constraints on the environment (in particular, on the control object), control cycle invariants, and 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 annotated Reflex programs uses the global clock and the local clocks of individual processes, the time of which is measured in the number of control cycle iterations, to simulate time constraints on process execution in certain states. It stores a complete history of changes in the values of the shared variables for a more complete description of time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of controlling transitions of processes from state to state and the interaction of processes with each other and with the environment. E