LTL Specification for the Development and Verification of Logical Control Programs in Feedback Systems

—This article continues a series of publications on the development and verification of control programs based on a special type of linear temporal logic (LTL) specification. Previously, a declarative LTL specification was proposed to describe strictly deterministic program behavior, and methods for its verification and translation were developed: the nuXmv model checker is used for verification, and translation is carried out into the imperative programming language ST for programmable logic controllers (PLCs). When verifying a declarative LTL specification of program behavior, it may become necessary to model the behavior of its environment. In general, it is important to ensure the possibility of constructing closed-loop systems comprising both the control program and its environment. In this paper, an LTL specification of limited nondeterministic behavior of a Boolean variable is proposed to describe the behavior of the environment in logical control programs. This specification allows specifying the behavior of Boolean feedback signals and the fairness conditions to exclude unrealistic behavior scenarios. The article presents an approach to the development and verification of logical control programs in which the behavior of the program’s environment is modeled as constraints on the behavior of its input signals, avoiding the need to explicitly model the environment’s internal processes. As a result, the constructed closed-loop “program-environment” model offers a number of advantages: simplified modeling, reduced state space of the model being verified, and decreased verification time. When the behavior of the environment cannot be reduced to the behavior of the existing input signals, this approach allows the use of “imaginary” sensors—additional Boolean variables used as an auxiliary means for describing the behavior of the input signals. The purpose of introducing imaginary sensors is to compensate for the missing sensors for tracking the specific behavior of individual elements of the environment, which must be taken into account when specifying the realistic behavior of the inputs of the logical control program. The proposed approach to the development and verification of programs taking into account the behavior of the environment (controlled system) is demonstrated using the example of an industrial plastic molding plant.