LTL-specification for development and verification of logical control programs in feedback systems

M. V. Neyzov ; E. V. Kuzmin

Modelirovanie i analiz informacionnyh sistem, Tome 31 (2024) no. 3, pp. 240-279

Résumé

The article continues the series of publications on the development and verification of control programs based on LTL-specifications of a special type. Earlier, a declarative LTL-specification was proposed to describe the strictly deterministic behavior of programs, ways of its verification and translation were worked out: for verification, the model checking tool nuXmv is used, and the translation is carried out into an imperative programming language ST for programmable logic controllers. When verifying the declarative LTL-specification of the behavior of programs, there may be a need to simulate the behavior of its environment. In general, it is required to ensure the possibility of constructing closed-loop systems “program-environment”. In this work, an LTL-specification of constraintly nondeterministic behavior of a Boolean variable is proposed to describe the behavior of the environment of logical control programs. This specification allows defining the behavior of Boolean feedback signals, as well as fairness conditions to exclude unrealistic scenarios of behavior. The article proposes an approach to the development and verification of logical control programs, within which the behavior model of the program environment is described in the form of constraints on the behavior of its input signals, what allows avoiding a separate detailed representation of the processes of the environment operation. As a result, the obtained behavior model of the closed-loop system “program-environment” provides a number of advantages: simplification of the modeling process, reduction of the state space of the verified model, and reduction of verification time. If it is impossible to reduce the behavior of the environment to the behavior of existing input signals, this approach suggests using “imaginary” sensors — additional Boolean variables that are used as an auxiliary means for describing the behavior of input signals. The purpose of introducing imaginary sensors is to compensate for missing sensors to track the specific behavior of some elements of the environment that needs to be taken into account when defining realistic behavior of the inputs of a logical control program. The proposed approach to the development and verification of programs taking into account the behavior of the environment (a control object) is demonstrated by the example of an industrial plastic molding plant.

Détail

Keywords: control software, PLC program, declarative LTL-specification, LTL-specification of constraintly nondeterministic behavior, fairness conditions, closed-loop systems verification, plant behavior model, imaginary sensor, temporal properties, model checking, nuXmv verifier, SMV-specification.