In the paper the possibility of utilization of the Kripke structures for applying linear-time temporal logic in problems of verification of reactive systems is considered. The definition and main characteristics of the cyberphysical systems, finite state machines, Kripke structures and temporal logics are considered by the authors. Example of modeling on the base of GOLDi is provided.
With the high complexity of modern computer systems (millions of lines of code and billions of transistors), it is impossible to completely avoid errors. It is not only related to the application software developed in a short time in a competitive market environment, but also to critical components, such as hardware (I/O devices, microprocessors) and software (compilers, operating systems). It is obvious that the systems, in the design and implementation of which mistakes are made, can in one or another situation behave in unpredictable ways and lead to serious consequences. The literature describes many cases of this kind. As vivid examples following can be represented.
In 1996, the launch vehicle Ariane 5, developed by the European Space Agency,
exploded at the 39th second after launch. As it turned out later, the onboard system
partially used the software of the previous version of the rocket, the Ariane 4, in
particular, the inertial navigation system control module [
Another notable example is the case of the medical device Therac-25 [
It is important to understand that errors in computer systems are not exceptional.
According to statistics, the average number of errors per thousand lines of
undebugged code ranges in 10-505 [
Verification is the process of checking of the compliance of a program (its model) with the requirements placed on it. If the program meets the requirements, it is called correct. Otherwise, the program is called incorrect, and the fact of non-compliance of the program with the requirements is an error. Thus, verification is the analysis of the program for the presence or absence of errors in it. An indefinite verdict is also possible when errors are not found, but their absence has not been proven.
It is necessary to take into account many nuances. First, the requirements, as a rule, are formulated informally, in natural language, so it is not always possible to unambiguously determine whether the program corresponds to them or not. Secondly, proving the absence of errors in the program is extremely difficult from a mathematical point of view (because of the fact that this task is not fully amenable to automation).
Verification methods can be divided into three main groups [
Each of the specified groups of methods has its advantages and disadvantages, each has its own area of applicability. Full verification of complex systems of responsible purpose is impossible without the joint use of different approaches. This work focuses on mostly formal methods of verification programs. 2.2
Formal verification is based on mathematical (logical) modeling programs and requirements for them. The idea is exactly the same as when using models in other areas of knowledge: ─ a model is created – an idealized description of the object or phenomenon under study; ─ the model is investigated using mathematical methods; ─ research results are transferred to a real object or phenomenon.
Of course, the applicability of this approach is determined by the models used – it is necessary to clearly understand the conditions for their adequacy.
The general process of formal verification [
For the presentation of program models and requirements models, the languages of the formal specification of programs (modeling languages) and the languages of the formal specification of requirements are used respectively.
Formal verification methods differ in the types of program models (state machines, Petri nets, labeled transition systems), types of requirements models (software contracts, production rules, temporal statements), correspondence relations (equivalence, simulation, route inclusion) and compliance verification techniques (state space research, symbolic analysis, deductive inference). In this paper we briefly consider one of the most popular formal verification methods – model checking. In model checking, requirements for programs are represented by logical formulas of a certain type, and programs themselves are structures interpreting formulas of this type; the correspondence relation is the truth of a formula on a structure (a program satisfies the requirements if and only if the corresponding structure is a model of the corresponding formula).
Often, temporal logics are used to represent the requirements – logic that allows one to define the relationship of events in time, for example, Linear-time Temporal Logic or Computational Tree Logic. Accordingly, Kripke structures and related formalisms (marked transition systems) are used to represent programs.
Kripke structures are used to model reactive systems – systems operating in an
“infinite loop” and interacting with their environment. As an example of such systems
cyber-physical system can be seen. The behavior of the system is modeled by
calculation in the Kripke structure [
Propositional temporal logic can be used to describe requirements, in particular LTL. The main method for establishing the correctness or incorrectness of a model is to search in the state space (bypassing the state graph). 3
A finite state machine (FSM) is a computation model that can be implemented with
hardware or software and can be used to simulate sequential logic (for example
computer program) [
There are two types of finite state machines: deterministic finite state machines (deterministic finite automaton) and non-deterministic finite state machines (nondeterministic finite automata).
A deterministic finite automaton (DFA) is described by a five-element tuple: Q, , , q0 , F . (1)
Where Q is a finite set of states, is a finite, nonempty input alphabet, is a series of transition functions, q0 is the starting state, F is the set of accepting states.
There must be exactly one transition function for every input symbol in from each state. DFAs can be represented by following diagrams:
Similar to a DFA, a nondeterministic finite automaton (NDFA) is described by an above five-element tuple. Unlike DFAs, NDFAs are not required to have transition functions for every symbol in , and there can be multiple transition functions in the same state for the same symbol. Additionally, NDFAs can use null transitions, which are indicated by . Null transitions allow the machine to step from one state to another without having to read a symbol. NDFAs can be represented by diagrams of this form:
One might assume that NDFAs can solve problems that DFAs cannot, but NDFAs are just as powerful as DFAs. However, a DFA will require many more states and transitions than an NDFA would take to solve the same problem. Converting from DFA to NDFA and vice versa is possible which makes them equivalent. A system where particular inputs cause particular changes in state can be represented using finite state machines. This example describes the various states of a turnstile. Inserting a coin into a turnstile will unlock it, and after the turnstile has been pushed, it locks again. Inserting a coin into an unlocked turnstile, or pushing against a locked turnstile will not change its state. Diagram of the turnstile FSM is following:
Saul Aaron Kripke introduced structures named after him to the logical and
philosophical use in the late 1950s [
Such systems respond to environmental events by performing certain actions in
response. This is an extensive class of programs, including cyber-physical systems,
operating systems, device drivers, telecommunication environments, control systems,
etc. [
Cyber-physical systems are the systems that provide the integration of computing,
physical processes and networks, or as systems where software and physical
subsystems are closely bounded, each of which works in a variety of temporal and spatial
dimensions, demonstrating clear and multiple behavioral patterns, and interacts in a
variety of ways [
In general, the qualitative properties of cyber-physical systems can be classified into the following two broad categories: ─ reachability or guarantee properties that raise the question of whether a system can achieve a configuration that satisfies a particular property; ─ security properties that raise the question of whether the system can remain forever in configurations that satisfy a particular property.
The main properties of cyber-physical systems include following [
The behavior of cyber-physical systems is described in terms of sequences of events distributed in time. So-called temporal logics are often used for the specification of requirements for cyber-physical systems. Temporal logics are formal languages that allow to define the interrelationships of events in time: causal relationships, restrictions on the relative order, the magnitude of delays between events, etc. The following examples can be cited as temporal properties: the system always works without freezing; two users cannot simultaneously access shared data; a request with a higher weight will be processed before constipation with a lower weight. 5.2
Among number of temporal logics, two have become particularly popular in computer
science: Linear-time Temporal Logic (LTL) [
In LTL, two temporal operators are added to the syntax of classical propositional logic: the unary operator X (next time) and the binary operator U (until). These two operators form the LTL temporal basis.
Let a set of elementary statements (Atomic Propositions) be given. The LTL
formula is given by the following grammar [
Here, p is an arbitrary elementary statement from the AP set. For convenience, in LTL formulas it is possible to use: ─ derived logical connectives, for example, and ; ─ logical constants, true and false ; ─ derived temporal operators, for example F (in the Future), G (Globally), W (Weak until) and R (Release).
Temporal operators can be interpreted as following. ─ The formula is true at the next point in time – X . ─ The formula is true now or will surely become true in the future, but up to this point (not inclusive) the formula should be true – U . ─ The formula is true now or will become true sometime in the future – trueU which is also can be displayed as F . ─ The formula is false now and will never become true in the future (always, from now on, the formula is true) – F which is also represented as G . ─ The formula is true until the formula is not become true, without requiring the formula to ever become true in the future – U G or W . ─ The formula is true until the moment (inclusive) when becomes true the first time; if such a moment never comes, the formula is always true (it possible to say that frees ) – U or R .
Thus, the requirements for the system, which simulates a door lock and was described above, can be expressed in LTL logic: ─ G lock unlock – for system it is impossible to open and close door at the same time; ─ G locked lock – system should never close the closed door; ─ G lock X locked – if the door is closed, at the next moment in time it will become closed. 6
Integrated Communication Systems Group at the Ilmenau University of Technology
has many years of experience in integrated hard- and software systems and over 10
years of experience in dealing with Internet-supported teaching in the field of digital
system design [
Online laboratories offer various features like visualization and animation, which
allows to observe and to test all the properties of the design. In connection with
formal design techniques, simulation and prototyping are used to establish a foundation
for the development of a reliable system design. To check the functionality of the
whole design, some special simulation and validation features are included as integral
part of the GOLDI system. This offers various possibilities for the execution of
simulations [
GOLDI offers a Web-based environment supporting the above mentioned features to generate and execute a design by using simulation models.
As an example of modeling it was decided to create Kripke structure of the elevator which is located in the GOLDi. This elevator has ability to move upwards and downwards from floor to floor and open or close its door.
The atomic propositions for the Kripke structure representing the elevator are as follows: ─ 1st – elevator is located at the 1st floor; ─ 2nd – elevator is located at the 2nd floor; ─ DO – door is open; ─ MU – elevator is moving in the upward direction; ─ MD – elevator is moving in the downward direction.
For clarity, each state is labeled with both the atomic propositions that are true in the state and the negations of the propositions that are false in the state. The labels on the arcs indicate the actions that cause transitions and are not part of the Kripke structure. Kripke structure of the elevator can be seen at Fig.7.
This model can be used for further formal verification. For example one might want to determine that “door of the elevator is closed and it is moving upwards”. S0 , p 1st 2nd DO MU MD . Using Kripke structure this can be determined. 7
In the paper the authors considered the possibility of utilization of the Kripke structures for applying linear-time temporal logic in problems of verification of reactive systems. Review of the main characteristics of the cyber-physical systems, finite state machines, Kripke structures and temporal logics was carried out by the authors. Example of modeling on the base of GOLDi was provided in the paper.