Content area
This work continues the series of articles on the development and verification of control programs based on the LTL-specification. The approach consists in describing the behavior of programs by special form of linear temporal logic (LTL) formulae. The developed LTL-specification can be directly verified with the help of a model-checking tool. Next, according to the LTL-specification, a program code is unambiguously built in the imperative programming language. The specification is translated into the program using a template. The novelty of the work is the proposal of two new LTL-specifications, which are declarative and imperative, as well as in a stricter formal justification of this approach to program development and verification. A transition is made to nuXmv, a more advanced verification tool for finite and infinite systems. It is proposed to describe the behavior of control programs in a declarative manner. For this purpose, a declarative LTL-specification is intended, which defines a transition system as a formal model of program behavior. This behavior description method is quite expressive—the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to build a program code in the imperative language, the declarative LTL-specification is converted to an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications determine the same behavior. The imperative LTL-specification is translated into an imperative program code according to the presented template. The declarative LTL-specification, which undergoes verification, and the control program based on it are guaranteed to determine the same behavior in the form of a corresponding transition system. Thus, in the verification a model coherent with the actual behavior of the control program is used.
INTRODUCTION
When solving control tasks, a design system is naturally divided into the control system and the control object. In the operation process, they influence one another. The software implementing the control process is the control software (CSW) and is designed as a control system or as its part. The control object might be of a different nature and purpose. For example, in a cyber-physical system [1, 2], CSW forms an impact on the physical environment by interacting with it through sensors and actuators. Thus, the program of a programmable logic controller (PLC) [3] controls the technological process at the plant. In this case, the CSW is part of the hardware-software control system. Another example is a database management system, in which the CSW performs various handling operations with a data by managing their extract and storage. In this case, the control object is represented by the body of data that is not physical in essence but is a kind of software like the control system. When solving computational tasks, the designed system contains only software components. According to the work [4], a discrete information converter is represented as an automaton model consisting of interacting components, which are an operational automaton and a control automaton. The operational automaton transforms information, whereas the control automaton manages the actions of transforming it, that is, describes the computation control process. Focusing the control task in software development is typical of the approach known as software cybernetics [5]. In this approach, the control and the operational automata are implemented as software components at any level of abstraction, which is determined bythe task being solved [6]. Thus, the CSW can be developed as a separate part of the designed system when solving not only the control but also computational tasks.
The CSW is a reactive system [7, 8]. It is engaged in continuous cyclic interaction with the control object at the pace of its ongoing processes. The operation cycle of the reactive system consists of receiving input data and recording them in the input variables of the program, which calculates and updates the internal and output variables, and transfer of the values of the output variables to the control object.
High reliability and safety [9] requirements may be imposed on systems during their design. Some of the requirements inevitably turn into the CSW’s correctness requirements. Correctness means compliance with the given set of behavioral properties. The compliance checking procedure is called verification [10]. Strong compliance guarantees are ensured by formal verification methods [11]. One of these methods is model checking [12–15]. It requires having a model that is coherent with the actual behavior of the CSW.
This study continues the series of articles on developing and verifying PLC control programs on the basis of LTL-specification [16–25]. This approach proposes to develop the program behavior LTL-specification that can be verified directly by the model-checking method. Moreover, the specification is constructive; i.e., it can be used to unambiguously built a program in a certain programming language (ST [16, 22], LD [23], IL [24], CFC [18]) of the IEC standard 61131-3 [26] and the behavior model in the source language of verifier Cadence SMV (http://www.mcmil.net/smv.html). The LTL-specification has sufficient expressiveness for describing any computational process [17]. For LTL-specifications of counter machines see [19, 20]. In addition, it is proposed to use the LTL-specification for describing the consistent behavior of sensors [25] that is necessary for checking some program properties.
Novelty. This work proposes a more concise modification of the LTL-specification. A strict formal justification of its constructiveness and expressiveness is provided. The transition to nuXmv (https://nuxmv.fbk.eu), a more advanced tool for verifying finite and infinite systems, is performed.
Content of work. Section 1 exposes the control program development concept and presents the architectural features of the designed CSW. Section 2 contains used behavior models represented by the transition systems. The notions of complete and pseudo-complete transition systems are introduced. Section 3 exposes the syntax and semantics of the LTL language. Section 4 introduces a declarative and an imperative LTL-specification. The declarative specification is intended for describing the software behavior, whereas the imperative specification is intended for building the program code. The theorem of the equivalence of these LTL-specifications is proved. Section 5 assesses the expressiveness of the declarative LTL-specification in terms of Turing completeness. The Minsky counter machine is presented as an algorithm model equivalent to the Turing machine by computational capabilities. An example of a counter machine for squaring a number is provided. The theorem of the Turing completeness of declarative LTL-specification is proved. Section 6 formulates the verification problem. A constraint is imposed on the problem to make it solvable. Section 7 contains an example of the development and verification using the tool nuXmv of a declarative LTL-specification for the number-squaring PLC program. Section 8 presents a scheme of building an ST program by the imperative LTL-specification. The ST code of the number-squaring program is provided. Then, a conclusion is drawn. The application shows the building of the LTL-specification proposed in the Turing completeness theorem.
1 CONTROL PROGRAM DEVELOPMENT CONCEPT
A control program works in cycles. In each control cycle, the value of a variable either changes or remains unchanged. In this article, the emphasis is placed only on changes in variable values because they are the ones that bear the key semantic charge in control tasks. In control processes, it is always known why the state of a control object needs changing, why, for example, a particular device must be on or off. The reasons for changing variable values are declared as an LTL-specification. In addition, the specification describes the way these changes occur.
On the whole, the behavior of a program is the sum of the behaviors of all of its variables . This set contains input and internal/output variables. Originally, the behavior of all of the variables from is not declared and is absolutely nondetermined. Then, only internal/output variables are subject to declaration. The declaration imposes certain constraints on their behavior, after which it becomes strictly determined. The remaining nondeterminism of the input variables is necessary for preserving the diversity in the behavior of the determined program because the behavior of the input variables determines the behavior of the internal/output variables. To lose none of the program run scenarios, it is necessary to feed to the program input any permissible values in any succession, which is implemented by the nondetermined behavior of the inputs.
To analyze and declare the causes of changes in a variable, it is often required to know its previous value. For example, to determine the button press instant (pulse leading edge), it is necessary to know whether the button was pressed in the previous operating cycle. For this purpose, the set of auxiliary variables is introduced that store the previous values of the respective variables from . The behavior of the auxiliary variables is not declared and is always known. When the variables from are used, it can be considered that the leading underscore sign “_” is the pseudooperator of turning to the previous value of a respective variable from . By comparing the values of variables and (where ), it can be judged whether the value of variable has changed.
Then, the declaration in the form of an LTL-specification is verified and the program is built according to this specification. The constructed program has two features:
(1) The value of each variable changes not more than once per control cycle.
(2) The value of each variable changes only in one place of the program in some simple operator unit.
These two features allow having a clear and transparent idea about the way the value of a particular variable changes with the transition of the program from one state to another. It is established for each variable that its new value is clearly dependent on the previous values, which were obtained during the program execution in the previous operation cycle run, and on the new variable values calculated at the program execution in the current operation cycle run. The condition for changing the variable value only in one place of the program facilitates debugging and allows simply estimating the degree of readiness of the program and of the volume of its text. It is obvious that, during one operation cycle run, the value of any variable rises, declines, or remains unchanged relative to the value obtained in the previous operation cycle run. If we do not turn to the variable for assigning some value to it, the variable will retain its previous value.
2 TRANSITION SYSTEM AS PROGRAM BEHAVIOR MODEL
Assume that the program has main variables , …, and auxiliary variables , …, , which take values from the respective domains , …, . The infinite (in general) set will be the space of all possible states of the program. Set contains input and internal/output variables. Vector of variable values describes a specific state of the program and contains the current values of input variables and the values of internal/output variables calculated on the basis of the former. Variables , …, store the previous values of variables , …, . Each control cycle has the corresponding state transition. If the state remains unchanged, it is considered that a loop-like transition to this same state occurs.
All possible transitions form the program behavior. Let us accept as the program behavior model the transition system where is the set of states, infinite in general, is the set of initial states, is the total relation of transitions, is the set of atom assertions about the values of variables , …, and , …, , and is the function of state labeling by atom assertions. The totality of the relation of transitions means that there exists transition from any state .
The transition system graph is the one whose vertices and arcs are the states from and the transitions from, respectively. In the system of transitions, a path is the infinite sequence , where , . The path forms an infinite route in the graph of the transition system. The transition system LTS presets the set of paths originating from the initial states as
where is the set of all infinite words from alphabet and is the ith state of path .
The behavior model of the program with a nondetermined behavior of all of its variables , …, , , …, will be the complete transition system , where . Unlike LTS, the cLTS system has a transition relation that presets the complete graph of transitions by states. In fact, absolute nondeterminism always makes it possible to switch from any one state to any other state, including the state itself. It should be noted that the program with a nondetermined behavior of all of its variables (absolutely nondetermined program) contains the behavior of any other program with this same set of variables . Here, , so that cLTS contains any path starting from any state.
If the constraint in the form of the earlier described behavior of variables is imposed on the complete transition system cLTS, the result will be the pseudo-complete transition system , where , . The pseudo-complete transition system pLTS contains the behavior of any other program that retains the previous values of variables in variables .
With the declaration of the behavior of variables , certain limitations are imposed on the pseudo-complete transition system pLTS. As a result, the behavior model of the LTS program is derived from the pseudo-complete transition system pLTS by eliminating transitions that violate the preset behavior declaration.
3 LTL LOGIC LANGUAGE
Linear temporal logic (LTL) or linear-time temporal logic is an expansion of classical propositional logic with the help of modal operators that allow considering the temporal aspect in event sequences [12–15]. LTL is an important means of formal verification, where it is used to describe requirements on hardware and software systems [8, 27].
We shall use LTL for the following tasks:
• describing requirements on the pseudo-complete transition system pLTS to form the behavior model of the LTS program from that system;
• describing requirements on the behavior model of the LTS program to verify these requirements.
At , the LTL formulae behave according to the following grammar:
In addition to classical Boolean operators, an LTL formula might contain temporal operators as well: means that formula must be fulfilled in the next state, requires that be fulfilled in some future state, guarantees that will be fulfilled in the current and all future states. Formula means that must be fulfilled in the current or future state, whereas must be fulfilled in all the previous states. Operators and are binary: . That being said, operator is a special case of applying operator , namely, .
Let us define by induction the feasibility relation of the LTL formula for the arbitrary state of some path of the system of transitions, where , :
Let us also define the semantics of relation on paths and systems of transitions:
Formula is fulfilled on path , when it is fulfilled in the initial state of this path but on path set , when it is fulfilled on all of its paths. Formula is fulfilled in the state of the transition system LTS when is fulfilled for all of the paths in LTS that start with state . Formula is fulfilled in the transition system LTS when is fulfilled for any initial state . Let us use to define the set of all of the paths in LTS for which formula holds, that is, .
4 LTL-SPECIFICATION OF PROGRAM BEHAVIOR
4.1 Declarative and Imperative LTL-Specification
To preset the behavior of program variables , the declarative LTL-specification is used. For variable it includes formulae (1) and (2). They describe the way the variable changes in value:
1
2
In this case, is the condition (logical expression) that must be fulfilled for changing the value of variable v according to expression , . Expressions and are made up over the set of variables , where and , with the help of constants and logical and arithmetic operators, as well as comparison operators. That being said, it is assumed that, at any values of the variables from , the following conditions are fulfilled for these expressions: (1) variability condition , and (2) orthogonality condition , at .
The LTL formula (1) assumes that, if variable changes in value (the new value differs from the old value ), only one of conditions is true, whereas variable takes the value of expression . The LTL formula (2) is structurally rigid and consists of elements of formula (1). Formula (2) asserts that, if variable does not change in value (this value remains equal to the previous value ), then none of conditions is true. Prefix means that the assumption in brackets always holds starting from program operation cycle 1; i.e., it does not cover only the initial state .
In formula (1), the variability condition prevents the contradiction that might arise when expression is equal in value to the previous value of variable and the orthogonality condition is intended for complying with determinism in the behavior of this variable.
Without considering the initial program state , the variability requirement is recorded as the following LTL formula:
3
which means that, on condition that is true, expression must return a value different from the previous value of variable .
Similarly, for the orthogonality condition, there is a set of LTL formulae ( at ):
4
which means that not more than one condition can be valid.
If conditions (3) and (4) are met, the conjunction of a set of formulae of type (1) and (2) for the internal/output variables from forms the declarative LTL-specification of the behavior of noninitialized program .
For initialization, the LTL formula will be used in a special form without temporal operators: , where is the predicate setting constraints on the main variables. The initial values of auxiliary variables , …, always coincide with the initial values of the respective main variables.
The formula recorded as will be called the declarative LTL-specification of a certain program. Based on the pseudo-complete transition system pLTS, this formula defines the transition system LTS. This transition system will contain only those paths that correspond to the possible operating scenarios of the considered program.
Let us showcase the idea of specification by a simple example. Preset the behavior of one Boolean variable so that its value will not change after the zero-to-one transition. This behavior is depicted as a graph (Fig. 1). The graph vertices correspond to values of variable (states), whereas the arcs correspond to possible state transitions. It is seen in the graph that it is forbidden to preserve the value of 0 and change the value from 1 to 0 (the respective arcs are crossed out).
[See PDF for image]
Fig. 1.
Behavior of variable .
The program will have two Boolean variables and . The potential number of the program’s states is , and we designate them as , , , . Each state is a unique vector of values of variables and . In a graph vertex, the respective values of variables and are indicated above and under the line (Fig. 2a).
[See PDF for image]
Fig. 2.
State notation (a), complete transition system (b), pseudo-complete transition system (c).
The behavior of the absolutely nondetermined program with variables and is described by the complete transition system cLTS (Fig. 2b). In this case, the transition from any one state to any other state is possible, including the state itself. If variable will preserve the previous value of variable , then this will impose a certain constraint on the behavior of the program. Any possible behavior of this program is described by the pseudo-complete transition system pLTS (Fig. 2c). Here, there are no transitions that violate the equality of the current value of variable to the value of variable at the previous step (in the previous state). For example, there is no transition from to because, in state , variable , although, in the previous state , . In other words, the previous value of variable is not preserved in variable . Moreover, the other way round, the transition from to does take place because the previous value of variable is retained in variable : in state , and, in state , .
Let us describe the behavior of the program in the form of the declarative LTL-specification. In this case, this specification consists of only two formulae:
These formulae preset those requirements that are outlined in Fig. 1:
(1) The only reason, why the value of variable changes, is its zero value (the zero-to-one transition is permitted, whereas the one-to-zero transition is forbidden).
(2) If this reason exists (), the variable will inevitably change in value (the zero-to-zero loop is forbidden).
According to formula , if the value of variable changed, then its preceding value was zero and the change consisted of the inversion of this value (formalized point 1). As fixed by formula , if the value of variable did not change, its preceding value was not 0. This is equivalent to the assertion that if the preceding value of variable is 0, the value of the variable has changed (formalized point 2).
Let us see how each formula corrects the pseudo-complete transition system pLTS (Fig. 2c). Formula is violated in state when a piece of the path of nonzero length emanates from this state to state , where the left part of the implication is true and the right part is false. In our case, . Here, is not equal to (the left part of the implication is true) and is not 0 (the right part of the implication is false). This is why, any fragment of path leading to state is the counterexample that violates the validity of formula . and are examples of these fragments. Thus, formula is violated in pLTS (Fig. 2c), that is, . To make this impossible, let us eliminate all of the arcs included in state (Fig. 3a). Now, there are no counterexamples violating formula.
[See PDF for image]
Fig. 3.
Transition system that satisfies (a), and (b), initialized program (c).
Similarly, formula is violated in state , when a fragment of a path of nonzero length emanates from this state to state , where the left part of implication is true and the right part is false. In this case, . Here, = (the left part of the implication is true) and = 0 (the right part of the implication is false). This is why any fragment of the path leading to state is a counterexample violating the validity of formula . and are examples of these fragments. Thus, formula is violated in a pLTS that meets formula (Fig. 3a). To make this impossible, let us eliminate all of the arcs included in state (Fig. 3b). Now, there are no counterexamples violating formulae or . The presented LTL-specification of the behavior of variable was used to select from the pseudo-complete transition system pLTS only those paths in which the specification formulae and are fulfilled.
Let us fix one initial state of the program, that is, . For this purpose, add the following LTL formula of initializing . This formula is fulfilled only in state (entry arrow in Fig. 3c). No path can start from the other states (Fig. 3b); otherwise, this would violate formula . States are reachable from the initial state , which is why they can be used to form paths. State is not the initial state, cannot be reached from state , and cannot form paths in compliance with formula . Let us eliminate unreachable state and the arcs incidental to it; thus, the transition system of the initialized program is derived (Fig. 3c). This transition system defines the set of paths where all the specification formulae are valid.
Let us track the behavior of variable . Initially, in state , this variable has a value of 0. Then, the value necessarily changes to 1 (the inevitable transition to state occurs). After that, the value of variable does not change any longer (after the transition to state , where , looping in this state occurs). Thus, this transition system exactly predetermines the behavior of variable , shown in Fig. 1.
Defining a transition system using an LTL-specification. The pseudo-complete transition system is used to define the transition system with the help of the declarative LTL-specification. This system describes the behavior of the program. The transition relation is recorded as
where is the set of all of the paths of the transition system pLTS and is the final fragment of path, . Thus, from the pseudo-complete transition system pLTS, only those transitions are selected that form paths satisfying the formula φ.
The set of states is described as
i.e., contains only those states that are present in the selected transitions. The set of initial states is , where is the initialization formula from specification . The labeling function coincides with in set , that is, .
The declarative LTL-specification selects the path set from the pseudo-complete transition system pLTS. Formula corresponds to the transition system LTS constructed above. This system defines the selected path set as .
Conveyor system’s control task. Let us consider a simple case of specifying the behavior of a conveyor control program (Fig. 4). The conveyor carries the parts fed from the tray on the left to the tare on the right. The conveyor is equipped with two sensors: sensor one is the part detection sensor, and sensor two is the part weight sensor. When a part is detected by the part detection sensor, it sets ; when there is no part detected, the sensor sets . The readings of the part weight sensor take values from . Variable con taking values from is responsible for the work of the conveyor.
[See PDF for image]
Fig. 4.
Conveyor operation.
Assume that the conveyor is originally on and empty: . The behavior of entry variables ( and ), which show the values of the sensors, is not specified as LTL formulae, which is why it remains absolutely nondetermined.
Task 1. It is required to containerize the preset number of parts and then stop the conveyor. For this purpose, let us introduce a parts counter that takes values from . First, we describe the behavior of the program that counts the parts.
The initialization formula of the parts counting program is
The LTL formula describing the behavior of the parts counter is
If the value of counter has changed (the new value differs from the previous value), then the rising edge of the signal from the part detection sensor has been detected (only the new value is equal to one), and the change consists of increasing counter by one. Line two of formula assumes that, if the value of counter has not changed (the new and the preceding values are identical), then there has been no rising edge of the signal from the part detection sensor.
Consider the system of transitions of the parts counting program (Fig. 5b). For the designation of the states of this program, see Fig. 5a. Here, the values of variables n and d are shown above the bar, whereas the values of variables and are shown below the bar. The value of variable is highlighted in a frame.
[See PDF for image]
Fig. 5.
State notation (a), transition system of the parts counting program (b).
In Fig. 5b, all of the variables in the initial state have zero values. There are always two arcs emanating from any state: arc one is for the transition at the input signal , arc two is for the transition at the input signal . It is seen that, in any state apart from the initial state, variables and take values and , respectively, from the previous state. The transition system contains only those states in which the reason for an increase or preservation of the value of variable is reflected. This reason might be either the presence or the absence of a leading edge from the sensor. No other changes occur in variable because all the other states have been eliminated from the transition system. That being said, the transition system (Fig. 5b) has an infinite number of states, in which the value of variable rises monotonically from left to right.
Now, let us expand the program by adding to it the conveyor control procedure. The initialization formula for the expanded program is
After the defined number of parts are transported, the conveyor must stop. Let us record this with the help of the following LTL formula specifying the behavior of variable con:
If the value of variable con has changed, the conveyor was on, counter reached value , and the change consisted of turning the conveyor off. If the value of con has remained unchanged, then there was no right time for turning the conveyor off. The behavior specification of the entire program is recorded as the formula .
Task 2. It is required to containerize the set of parts with a total weight of and stop the conveyor. For this purpose, let us introduce weight counter that takes values from . In this case, the initialization formula of the program is
Let us define the behavior of the weight counter as
If the value of counter has changed, then the leading edge of the signal from the part detection sensor has been detected, whereas the change consists of the increase of counter by the weight of the part now placed on the metering underlayer.
After the parts of a defined weight are transported, the conveyor must stop. The LTL formula describing the behavior of variable con is
If the value of variable con changed, the conveyor was on, counter reached or surpassed the value of , whereas the change consisted of turning the conveyor off. The behavior specification of the whole program is formula .
Imperative LTL-specification. To build the imperative code of a program using the declarative LTL-specification, an intermediate formalization will be required in the form of an imperative LTL-specification. This specification is equivalent to the declarative LTL-specification (it expresses the same behavior); however, the former is directly converted to the imperative code of a program written, for example, in the ST language.
Taking into account (3) and (4), the imperative LTL-specification for variable v has the following form:
5
6
This specification describes the conditions and their corresponding rules for changing the value of variable in the if-then style.
4.2 Theorem on the Equivalence of the LTL-Specifications
Lemma 1.The satisfiability of the declarative LTL-specification implies the satisfiability of the imperative LTL-specification; i.e., under conditions (3) and (4), we have (1), (2)(5), (6).
Proof. Let us split the proof of the proposition into two parts. Part one will show the feasibility of inference (4), (1), (2) (5). Part two will show the validity of the logical inference (1) (6).
Let us prove part one of the lemma by applying the contraposition law to formula (2):
7
The result of applying (7) and (1) by implication transitivity is
Let us apply the expression in brackets to each condition of type :
The first conjunct follows from this:
8
The inference following from orthogonality condition (4) is
9
The result of combining formulae (8) and (9) is
Let us apply the expression in the right brackets to the first disjunct of the left brackets:
Part two of the formula is identically false. Let us reduce the expression as
10
At , formulae of this kind have a similar inference for other conditions . Having taken in the conjunction all of these formulae for all conditions , results in Eq. (5). Thus, the correctness of inference (4), (1), (2) (5) is proved.
Let us prove part two of the theorem. Having applied the contraposition law to (1), we shall have the following formula:
After the brackets have been removed, a certain disjunctive form:
We are interested in the first disjunct , whereas everything else has no meaning for the proof and is, therefore, replaced with the abstract expression . As a result,
Formula (6) follows from this. It thus appears that (1) (6). Lemma 1 is proved.
Lemma 2.The satisfiability of the imperative LTL-specification implies the satisfiability of the declarative LTL-specification; i.e., under conditions (3) and (4), we have (5), (6)(1), (2).
Proof. First, let us prove that (5), (6) (1). Transform (5) as
11
Apply the contraposition law to (6) to obtain
12
Combine (12) and (11):
Remove the first square brackets:
Equation (1) is derived from the latter formula. The validity of inference (5), (6) (1) is proved.
Now, let us prove that (3), (5) (2). Combine (5) and (3) to obtain
Apply the contraposition law to the latter formula:
Formula (2) has been obtained. Consequently, inference (3), (5) (2) is justified.
Lemma 2 is proved.
Theorem 1 (specifications equivalence). Declarative LTL-specification (1), (2) and imperative LTL-specification (5), (6) are equivalent provided that the variability condition (3) and orthogonality condition (4) are complied with.
Proof. It follows from Lemmas 1 and 2.
5 EXPRESSIVENESS OF DECLARATIVE LTL-SPECIFICATION
Let us evaluate the expressive capabilities of the declarative LTL-specification in terms of Turing completeness. To prove the theorem of the Turing completeness of the declarative LTL-specification, let us choose the Minsky counter machine [28–30] as a formal model of the algorithm. In terms of computational capabilities, this machine is equivalent to the Turing machine but seems more convenient for describing the behavior of programs: the Minsky machine has a more visually compelling program form, that is, a type of computer program written in a high-level language.
The Minsky counter machine M is the set , where is the finite nonempty set of control states of the machine; is the initial control state; is the conclusive or final control state; is the finite nonempty set of counters that can take values from ; is the set of rules of transitions between the control states of the machine; is the rule of transitions for the control state , where .
States , are divided in two types. Type 1 control states have transition rules of the form
13
where and . For type 2 control machines, the following transition rules are determined:
14
where . There are no transition rules contemplated for the final state . After entering the final state , the machine stops running.
The state (configuration) of the counter machine is set , where and , ; here, , … , are the values of the respective counters , … , .
The execution of the Minsky machine is the sequence of states , inductively determined according to the transition rules. The counter machine has one execution from the initial state because no more than one transition rule is contemplated for each control state.
After some set of counter values is fed to the input, the machine starts from the control state q1 and either stops in the control state qn, with the output set of counter values, or loops and thus implements a partial numerical function.
Let us consider as an example a three-counter Minsky 3cM machine that implements the function of squaring number , where . The rule of transition between the control states of the 3cM machine are as follows [29]:
15
The counter machine 3cM has eight control states , where is the initial control state and is the final control state. The set of counters is . It is assumed that, in the initial state, counter takes value , whereas the other two counters and have zero initial values. In the final state, the calculation result will be contained in counter at the zero values of counters and .
For the graphic representation of the rules of transitions between the control states of machine 3cM, see Fig. 6. In this figure, designation “” for counter corresponds to its increase by one, whereas “” indicates the tentative subtraction of one with transition to another control state along the right-hand arrow in the case of a zero value of counter .
[See PDF for image]
Fig. 6.
Graphical representation of number-squaring counter machine 3cM.
Theorem 2 (Turing completeness of LTL-specification). The behavior of any Minsky counter machine, i.e., the set of all its possible executions, can be specified using a declarative LTL-specification.
Proof. By way of proof, let us describe the general process of constructing the declarative LTL-specification of the behavior of a program that models the operation of an arbitrary Minsky counter machine.
Assume that there is some Minsky m-counter machine represented as a set of transition rules.
The program will contain the main variables and auxiliary variables .
Variable is intended for storing the number of the current control state and variables are intended for storing machine counter values. Thus, vector describes the current state of the machine. All program variables take values from . According to the transition rules, any transition of the Minsky machine corresponds to a transition between two program states. If none of the transition rules is followed for the current state of the machine, the machine remains in the same state. In this case, a loop transition to the same program state occurs in the program.
The program initialization formula describing the set of initial states will have the following form:
Then, let us execute the LTL formalization of transition rules for type 1 control states as follows:
16
The LTL formalization of transition rules for type 2 states takes the following form:
17
Let us split each type (16) formula into two LTL formulae:
18
Formulae (17) are fragmented as follows:
19
All of the counters have one and the same specification building procedure. Let us show how to build a specification for an arbitrary counter . Having grouped all of the formulae where counter is present, we obtain
20
Let us conjunctively combine the formulae in group (20) and add the formula describing the absence of change in the variable. We obtain the LTL-specification for :
21
Let us also show how to build a specification for variable . Let us group all of the formulae where this variable is present, and we obtain
22
Let us eliminate from group (22) the formulae in which , where .
Then, we shall conjunctively combine the remaining formulae and add the formula describing the absence of change in the variable. We obtain the imperative LTL-specification for :
23
Let us use the imperative LTL-specifications (21) and (23) to build the equivalent declarative LTL-specifications for and , respectively:
24
25
The declarative LTL-specification of the behavior of the program modeling the performance of the counter machine is an initialization formula and a set of formulae describing the behavior of variable (25) and all variables in the form (24). Formulae (25) and (24) comply with the variability condition (3) and orthogonality condition (4).
The procedure of building a declarative LTL-specification of the counter machine 3cM is described in the Appendix. Specification has the following form:
It should be noted that the latter formula of the LTL-specification can be simplified as follows:
The counter machine 3cM has eight control states , which is why variable . It is seen from the simple formula that the value of changes at . This indicates that the 3cM machine always switches to another control state. The only exception is the final control state in which the machine stops.
6 VERIFICATION OF THE DECLARATIVE LTL-SPECIFICATION
6.1 Formulation of the Problem
The original LTL-specification verification task
26
is the model-checking task; i.e., the task checking whether interpretation is a model of formula , where is the declarative LTL-specification defining a set of paths in the pseudo-complete transition system pLTS and is the verifiable LTL property.
We intend to solve this task with the help of the nuXmv software, a symbolic model-checking tool [12–15] that allows working with models with a finite and an infinite number of states.
It is important to note that, in the general case, task (26) is undecidable: there is no algorithm for checking the feasibility of formula in the interpretation of . If this procedure did exist, then it could be possible to find out for the counter machine cM the validity of , where is the declarative LTL-specification of the behavior of this counter machine and is its final state. In this way, it could be possible to solve the totality problem for Minsky counter machines. In other words, there would be an algorithm of defining for any counter machine, whether the machine will stop at all possible initial counter values. It is known, however, that the totality problem is not even partially decidable for two-counter Minsky machines [30].
To solve task (26), it is required for the set of states of the pseudo-complete transition system to be finite. For this purpose, the domain of values of each variable from , where , must be constrained. In this case, the finite transition system pLTS becomes a Kripke structure [12–15].
To correctly describe the behavior of finite programs, the declarative LTL-specification must comply with the additional condition of the constraint for each variable :
27
i.e., if condition is true (), expression returns the value , which belongs to the value domain of the variable in question. It will also be required for the initialization formula to contain expressions that ensure that the initial value of each variable falls within the permissible value domain.
For example, the declarative LTL-specification with constraint (27) allows specifying the behavior of a finite Minsky counter machine, which is a counter machine with constraints on the counter values and a modified transition rule for type 1 control states. The constraints are introduced through function . This function sets the upper threshold for each counter . The modified transition rule for type 1 control states is
In the next subsection of this section, a finite number-squaring counter machine will be considered as an example.
To check model (26) with the help of the nuXmv tool, it is necessary to specify the set of paths in some form that would be acceptable for this tool. Since and are already LTL formulae supported by nuXmv, the simplest solution will be not to transform them but to leave them as they are. That being said, according to the definition of LTL, task (26) can be reduced to the following task:
28
Here, the feasibility of implication in the pseudo-complete transition system pLTS is checked. In this case, the verifier will pass the set of all possible paths in pLTS and check the validity of property only in those paths where the specification of behavior is valid.
In this formulation of the verification task, it will be required to define the pseudo-complete transition system pLTS in the input language of the nuXmv verifier. For this purpose, it is necessary to declare two sets of variables and , and then describe the behavior of each auxiliary variable with the help of expression . This expression saves in the preceding value of the respective variable . In nuXmv, the behavior of the variables from is absolutely nondeterministic by default. After pLTS is defined, it is possible to launch the nuXmv tool for the feasibility check of the formula . If this formula is valid, the specification of behavior meets property ; otherwise, specification does not correspond to .
6.2 Finite Counter Machine for Number Squaring
Let us build finite counter machine for number squaring with the constraints , , and on counters , , and , respectively:
Let us present the declarative LTL-specification of the behavior of the finite counter machine inasmuch as this specification differs from the declarative specification of the original 3cM number-squaring machine. The only formulae that will change are , , , and :
Formula will remain unchanged because, in each type 1 transition rule for , both branches of the condition lead to the same control state. Therefore, the formula of the behavior of variable is simplified to the previous variant of.
Let us consider some LTL properties of the counter machine that must necessarily be met for any execution of this machine:
This property means that, if the counter machine starts at , , and and it enters the final control state , counters and will have zero values and counter will contain the target result :
This property requires constraining the aggregate value of counters and to throughout the entire runtime of the counter machine .
It is required that the value of counter does not go beyond throughout the entire runtime of machine :
From any control state, including the initial control state, machine always switches to the final control state sooner or later:
If the counter machine enters the final control state , it remains in this state forever:
The control state always takes values from 1 to 8.
Now, let us consider the LTL property that is violated in some execution of the counter machine :
This property asserts that, in each possible execution of machine , from certain initial states, the final result of its run in the control state differs from at . The counterexample corresponds to the machine execution at .
It should be noted that the specification of the arithmetic properties of machine that calculates the value of required the introduction of an input variable and its corresponding auxiliary variable , which were not present in the transition rules of machine . To check for the correctness of the properties of this kind, it is necessary to expand the pseudo-complete transition system pLTS by adding the values of and to its states. By simulating the input number to be squared, variable must retain its value throughout the calculation process. This is achieved by using a special subformula , included in the properties themselves. Expression requires the current value of variable to be always equal to its previous value, that is, that it does not change.
7 DEVELOPMENT AND VERIFICATION OF LTL-SPECIFICATION OF PLC PROGRAM
Let us implement the reactive system as a PLC program based on the number-squaring counter machine . The motivation for using this example is to show some abstract behavior of a control automaton without reference to the actual equipment and technological process. In this case, it might be considered that the technological process of production is the calculation of a squared number: input number acts as the original workpiece and is the finished product. The scheme of the system is presented in Fig. 7. The PLC responds to input signals from the buttons and feeds output signals to the indicators. The control automaton with state is a control system for process calculating squared numbers. The control object is a set of four variables, including n, a, b, and c. The control automaton exerts a control effect on this set of variables by increasing (inc) and decreasing (dec) their values. The control automaton can also read their values in any PLC operation cycle.
[See PDF for image]
Fig. 7.
Reactive system represented as a PLC program.
Assume that there is a control panel (see Fig. 8) with four buttons “Start”, “Reset”, “+1”, and “–1”; nine status lights “q0”–“q8”; and four indicators for showing values of counters , , and , and entry number . Buttons “+1” and “–1” set number that will be squared. The pressing of buttons “+1” and “–1” increases and, respectively, decreases by 1. Both buttons will respond only for the control automaton in the initial state . The other automaton states are inherited from counter machine . The “Start” button launches the calculation process for the current on condition that the automaton is in state . After the launch the value of variable is placed in variable , whereas and have zero values. The “Reset” button switches the automaton to the starting state from the final state that the automaton enters after finishing the calculation of number . That being said, counter resets to 0. Lamps “q0”–“q8” show the current status of the control automaton (the active status number is stored in variable).
[See PDF for image]
Fig. 8.
PLC control panel.
For the PLC interface, see Fig. 9. Here, buttons “Start”, “Reset”, “+1”, and “–1” are associated with Boolean variables PBStart, PBReset, PBPls, and PBMns, respectively. Program variables q,, , , and play the role of the PLC outputs leading to the corresponding lamps and indicators.
[See PDF for image]
Fig. 9.
PLC interface.
Since verification is done with the help of nuXmv, the specification and its properties will be recorded in the language of this verifier. In the nuXmv syntax, the declarative LTL-specification of the number squaring PLC program has the following form:
In the nuXmv verifier language, symbols “&”, “|”, “!”, and “–” mean logical operators “”, “”, “”, and “”, respectively.
It should be noted that the behavior specification of input variables PBStart, PBReset, PBPls, and PBMns is not performed because these variables might take any values at each new step of a PLC operation cycle. The constraints for variables , , , and are preset with the help of the corresponding constants , , , and .
It is seen that the program behavior specification is written as one large LTL formula. Let us denote it as .
Let us preset in the nuXmv syntax the specification of the properties of the number-squaring PLC program as a set of LTL formulae P1,…,P7:
Property P1 asserts that, in the final state , the result of calculating is in variable , whereas variables and are zero.
Property P2 asserts that the sum of and never exceeds .
Property P3 asserts that, during the calculation, the value of variable never exceeds .
Property P4 asserts that, if the calculation process has started (the automaton is not in the initial state ), then it will necessarily finish (in the future, the automaton will enter the final state ).
Property P5 asserts that if the “Start” button is pressed in the initial state , then the calculation process will be launched and finish in its final state .
Property P6 asserts that if the calculation process reaches the final state , then it either continues to remain in this state or enters the initial state at , , and after the “Reset” button is pressed.
Property P7 checks the variables for constraints: in states and , variable is smaller than ; in state , variable is smaller than ; and in state , variable is smaller than .
Each property is checked separately; i.e., the feasibility check , where is the specification of the behavior of the number-squaring program, is performed.
Let us describe the pseudo-complete transition system pLTS and the verifiable formula in the nuXmv syntax:
After the keyword LTLSPEC, the last line contains the formula to be checked for feasibility relative to the pseudo-complete transition system pLTS. In this line, Spec is the LTL-specification of the number-squaring program and Prop is any property from P1, …, P7.
Properties P1, .., P7 were checked for feasibility on a personal computer with an Intel Core i5-3570 3.4 GHz processor and 8-GB RAM. Properties P4 and P5 were checked for about two minutes and the other properties were checked for a few seconds.
8 BUILDING OF PLC PROGRAM BY LTL-SPECIFICATION
Let us use declarative LTL-specification from Section 7 to build the code of the number-squaring program in the ST language. For this purpose, it will be required to convert the declarative LTL-specification to imperative. In turn, the imperative LTL-specification (5), (6) for variable from the set has the following ST code-building pattern:
The ST program built on the basis of this pattern in the CoDeSys environment (https://codesys.com) has the following form:
When a program code is generated according to the LTL-specification, the IF-ELSIF units must be arranged as follows: a certain variable without the pseudooperator “_” can be used in the IF-ELSIF unit of another variable only if the IF-ELSIF unit of the former variable is already found earlier in the text.
For example, in the presented program, the IF-ELSIF unit of variable must precede the IF-ELSIF unit of variable , because, in the rules of forming a new value of , variable participates without the pseudooperator “_”; i.e., the new value of is generated from the new value of .
When the PLC program is built, each variable from the LTL-specification must be defined in a suitable variable description section, such as “inputs”, “outputs”, and “local variables”. Then, each such LTL-specification variable is initialized according to the specification and, specifically, according to the S0 LTL type of initialization formula. The PLC inputs are described in the VAR_INPUT section, the outputs are described in the VAR_OUTPUT section, and the other variables are described in the VAR section. Initialization is done in the variable declaration sections.
In addition, for a pseudo-complete transition system, the idea of the leading underscore pseudooperator operator “_” must be implemented. For this purpose, a place for a pseudooperator section is allocated at the very end of the PLC program. Assignments , where , are added to this section. That being said, it is also necessary to determine in the section describing variables with the same initial value as for variable .
In the LTS behavior model, the transition from one state to another will correspond to the execution of the PLC program up to the pseudooperator section. In other words, the state will be a vector of values of all program variables, which was obtained before the execution of assignments that implement pseudooperator “_”. The initial state is the state of the PLC program after initialization. The new state of the PLC program is constructed as follows: (1) the pseudooperator section is executed (except for the first time), (2) input variables (PLC inputs) take new values, and (3) the PLC program is executed from the beginning to the pseudooperator section. In this case, the behavior of the ST program is guaranteed to correspond to the original declarative LTL-specification.
CONCLUSION
This paper presents the declarative LTL-specification proposed for use in describing the behavior of the control programs. This specification allows describing the reasons and rules for changing the program variable values. The proposed behavior declaration method seems to be natural and convenient for control systems.
A transition system LTS is used as the program model. The pseudo-complete transition system pLTS contains the behavior of all the programs with the given set of variables. The declarative LTL-specification forms the behavior model of the program LTS by selecting only the necessary paths from the pseudo-complete transition system pLTS.
The declarative LTL-specification of the program can be directly verified by model checking using the nuXmv tool. For this purpose, it is necessary to set the nuXmv model of the pseudo-complete transition system. In the general case, the verification problem is undecidable for infinite models. To make the problem decidable, it is proposed to constrain the model by making the set of states finite. In this case, the transition system becomes the Kripke structure.
The declarative LTL-specification is constructive in the sense that the control program can be constructed from it. For this purpose, an auxiliary imperative LTL-specification is presented, for which its equivalence to the declarative LTL-specification is then proved. The imperative LTL-specification describes the behavior of a program in an imperative style that corresponds, for example, to the style of the ST programming language. Due to this, it is possible to directly translate the imperative LTL-specification into the ST program. The translation approach is tentatively described as a template. The translation scheme in question ensures complete compliance of the behavior of the resulting ST program with the original declarative LTL-specification.
The declarative LTL-specification is Turing complete. This is proved by a technique that allows constructing a declarative LTL-specification for an arbitrary Minsky counter machine, which is a formalism equal to a Turing machine. Turing completeness guarantees that absolutely any computational algorithm is described by the declarative LTL-specification. The LTL-specification building method is showcased by the number-squaring counter machine.
The results obtained during operation confirm the theoretical validity of the approach to development and verification of control programs based on the LTL-specification.
FUNDING
This work was supported as part of a state assignment by the Institute of Automation and Electrometry of the Siberian Branch of the Russian Academy of Sciences, project no. 122031600173-8, and by Yaroslavl State University, project VIP-016.
CONFLICT OF INTEREST
The authors of this work declare that they have no conflicts of interest.
Translated by S. Kuznetsov
Publisher’s Note.
Allerton Press remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
AI tools may have been used in the translation or editing of this article.
REFERENCES
1 Oks, S.J., Jalowski, M., Lechner, M., Mirschberger, S., Merklein, M., Vogel-Heuser, B., and Möslein, K.M., Cyber-physical systems in the context of Industry 4.0: A review, categorization and outlook, Inf. Syst. Front., 2022. https://doi.org/10.1007/s10796-022-10252-x
2 Lee, E.; Seshia, S. Introduction to Embedded Systems: A Cyber-Physical Systems Approach; 2017; 1371.68001
3 Parr, E.A. Programmable Controllers: An Engineer’s Guide; 2003; 0117.20401
4 Lifshits, V.N.; Sadovskii, L.E. Algebraic models of computing machines. Russ. Math. Surv.; 1972; 27, pp. 87-135. [DOI: https://dx.doi.org/10.1070/RM1972v027n03ABEH001379] 0251.94039
5 Cai, K.-Y., Chen, T.Y., and Tse, T.H., Towards research on software cybernetics, Proc. 7th IEEE Int. on High-Assurance Systems Engineering (HASE 2002), Tokyo, 2002, IEEE, 2002, pp. 240–241.
6 Polikarpova, N. and Shalyto, A., Avtomatnoe programmirovanie (Automata-Based Programming), Moscow: Piter, 2011, 2nd ed.
7 Harel, D. and Pnueli, A., On the development of reactive systems, Logics and Models of Concurrent Systems, Apt, K.R., Ed., NATO ASI Series, vol. 13, Berlin: Springer, 1985, pp. 477–498. https://doi.org/10.1007/978-3-642-82453-1_17
8 Pnueli, A., Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends, Current Trends in Concurrency, de Bakker, J.W., de Roever, W.P., and Rozenberg, G., Eds., Lecture Notes in Computer Science, vol. 224, Berlin: Springer, 1986, pp. 510–584. https://doi.org/10.1007/bfb0027047
9 Maurya, A.; Kumar, D. Reliability of safety-critical systems: A state-of-the-art review. Qual. Reliab. Eng. Int.; 2020; 36, pp. 2547-2568. [DOI: https://dx.doi.org/10.1002/qre.2715] 1448.35447
10 Rajabli, N.; Flammini, F.; Nardone, R.; Vittorini, V. Software verification and validation of safe autonomous cars: A systematic literature review. IEEE Access; 2021; 9, pp. 4797-4819. [DOI: https://dx.doi.org/10.1109/access.2020.3048047] 07452687
11 D’silva, V.; Kroening, D.; Weissenbacher, G. A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst.; 2008; 27, pp. 1165-1178. [DOI: https://dx.doi.org/10.1109/tcad.2008.923410] 1138.68444
12 Clarke, E.M.; Henzinger, T.A.; Veith, H.; Bloem, R. Handbook of Model Checking; 2018; Cham, Springer: 1390.68001
13 Karpov, Yu.G., Model Checking. Verifikatsiya parallel’nykh i raspredelennykh programmnykh sistem (Model Checking: Verification of Parallel and Distributed Program Systems), St. Petersburg: BKhV-Peterburg, 2010. https://www.elibrary.ru/sdrjqb.
14 Vel’der, S.E., Lukin, M.A., Shalyto, A.A., and Yaminov, B.R., Verifikatsiya avtomatnykh programm (Verification of Automata-Based Programs), St. Petersburg: Univ. ITMO, 2011.
15 Clarke, E.M.; Grumberg, O.; Peled, D.A. Model Checking; 2002; 1423.68002
16 Kuzmin, E.V.; Sokolov, V.A. Modeling, specification and construction of PLC-programs. Autom. Control Comput. Sci.; 2014; 48, pp. 554-563. [DOI: https://dx.doi.org/10.3103/S0146411614070244] 1185.68255
17 Kuzmin, E.V.; Ryabukhin, D.A.; Sokolov, V.A. On the expressiveness of the approach to constructing PLC-programs by LTL-specification. Autom. Control Comput. Sci.; 2016; 50, pp. 510-519. [DOI: https://dx.doi.org/10.3103/S0146411616070130] 1517.03036
18 Ryabukhin, D.A.; Kuzmin, E.V.; Sokolov, V.A. Construction of CFC-programs by LTL-specification. Autom. Control Comput. Sci.; 2017; 51, pp. 567-575. [DOI: https://dx.doi.org/10.3103/s0146411617070173] 1185.68255
19 Kuzmin, E.V. LTL-specification of counter machines. Autom. Control Comput. Sci.; 2022; 56, pp. 711-722. [DOI: https://dx.doi.org/10.3103/S0146411622070112] 1507.68191
20 Kuzmin, E.V. Linear temporal logic specification of bounded counter machines. Autom. Control Comput. Sci.; 2023; 57, pp. 683-695. [DOI: https://dx.doi.org/10.3103/S0146411623070064] 1523.46054
21 Kuzmin, E.V.; Sokolov, V.A. On construction and verification of PLC-programs. Autom. Control Comput. Sci.; 2013; 47, pp. 443-451. [DOI: https://dx.doi.org/10.3103/S0146411613070110] 1185.68255
22 Kuzmin, E.V.; Sokolov, V.A.; Ryabukhin, D.A. Construction and verification of PLC-programs by LTL-specification. Autom. Control Comput. Sci.; 2015; 49, pp. 453-465. [DOI: https://dx.doi.org/10.3103/s0146411615070159] 1185.68255
23 Kuzmin, E.V.; Sokolov, V.A.; Ryabukhin, D.A. Construction and verification of PLC LD programs by the LTL specification. Autom. Control Comput. Sci.; 2014; 48, pp. 424-436. [DOI: https://dx.doi.org/10.3103/s014641161407013x] 1185.68255
24 Ryabukhin, D.A.; Kuzmin, E.V.; Sokolov, V.A. Construction of PLC IL-programs by LTL-specification. Model. Anal. Inf. Sistem; 2014; 21, pp. 26-38. [DOI: https://dx.doi.org/10.18255/1818-1015-2014-2-26-38] 1185.68255
25 Kuzmin, E.V.; Ryabukhin, D.A.; Sokolov, V.A. Modeling a consistent behavior of PLC-sensors. Autom. Control Comput. Sci.; 2014; 48, pp. 602-614. [DOI: https://dx.doi.org/10.3103/s0146411614070256] 1185.68255
26 IEC 61131-3:2013 Programmable controllers, Part 3: Programming languages, International Standard, 2013. https://webstore.iec.ch/publication/4552.
27 Pnueli, A., The temporal logic of programs, 18th Annu. Symp. on Foundations of Computer Science (SFCS 1977), Providence, R.I., 1977, IEEE, 1977, pp. 46–57. https://doi.org/10.1109/sfcs.1977.32
28 Minsky, M. Computation: Finite and Infinite Machines; 1967; 0195.02402
29 Schroeppel, R., A two counter machine cannot calculate 2N, Artificial Intelligence Memo #257, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, 1972.
30 Kuzmin, E.V. Schetchikovye mashiny (Counter Machines); 2010; Yaroslavl, Yaroslavl. Gos. Univ.: 1204.68122
© Allerton Press, Inc. 2024.