Reflex is a process-oriented language that provides a design of easy-to-maintain control software for programmable logic controllers. The language has been successfully used in a several reliability critical control systems, e. g. control software for a silicon single crystal growth furnace and electronic equipment control system. 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 the formal operational semantics of Reflex programs extended by annotations describing the formal specification of software requirements as a necessary basis for the application of such methods. A brief overview 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 that allows to disengage from specific input/output ports. Types of annotations that specify restrictions on the values of the variables at program launch, restrictions on the environment (in particular, on the control object), invariants of the control cycle, 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 the annotated Reflex programs uses the global clock as well as the local clocks of separate processes, the time of which is measured in the number of iterations of the control cycle, to simulate time constraints on the execution of processes at certain states. It stores a complete history of changes of the values of shared variables for a more precise description of the time properties of the program and its environment. Semantics takes into account the infinity of the program execution cycle, the logic of process transition management from state to state and the interaction of processes with each other and with the environment. Extending the formal operational semantics of the Reflex language to annotations simplifies the proof of the correctness of the transformation approach to deductive verification of Reflex programs developed by the authors, transforming an annotated Reflex program to an annotated program in a very limited subset of the C language, by reducing a complex proof of preserving the truth of program requirements during the transformation to a simpler proof of equivalence of the original and the resulting annotated programs with respect to their operational semantics.

During the climb flight of big passenger airplanes, the airplane’s vertical movement, i.e. its pitch angle, results from the elevator deflection angle chosen by the pilot. If the pitch angle becomes too large, the airplane is in danger of an airflow disruption at the wings, which can cause the airplane to crash. In some airplanes, the pilot is assisted by a software whose task is to prevent airflow disruptions. When the pitch angle becomes greater than a certain threshold, the software overrides the pilot’s decisions with respect to the elevator deflection angle and enforces presumably safe values. While the assistance software can help to prevent human failures, the software itself is also prone to errors and is - generally - a risk to be assessed carefully. For example, if software designers have forgotten that sensors might yield wrong data, the software might cause the pitch angle to become negative. Consequently, the airplane loses height and can - eventually - crash.

In this paper, we provide an executable model written in Matlab/Simulink® for the control system of a passenger airplane. Our model takes also into account the software assisting the pilot to prevent airflow disruptions. When simulating the climb flight using our model, it is easy to see that the airplane might lose height in case the data provided by the pitch angle sensor are wrong. For the opposite case of correct sensor data, the simulation suggests that the control system works correctly and is able to prevent airflow disruptions effectively.

The simulation, however, is not a guarantee for the control system to be safe. For this reason, we translate the Matlab/Simulink® -model into a hybrid program (HP), i.e. into the input syntax of the theorem prover KeYmaera. This paves the way to formally verify safety properties of control systems modelled in Matlab/Simulink®. As an additional contribution of this paper, we discuss the current limitations of our transformation. For example, it turns out that simple proportional (P) controllers can be easily represented by HP programs, but more advanced PD (proportional-derivative) or PID (proportional-integral-derivative) controllers can be represented as HP programs only in exceptional cases.

The C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the C-kernel program and Hoare logic for the C-kernel as input. To solve the well-known problem of determining loop invariants, the definite iteration approach was chosen. The body of the definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the substitution operation rep, which represents the action of the cycle in symbolic form. Also, in our meta generator, the method of semantic markup of correctness conditions has been implemented and expanded. It allows to generate explanations for unproven conditions and simplifies the errors localization. Finally, if the theorem prover fails to determine the truth of the condition, we can focus on proving its falsity. Thus a method of proving the falsity of the correctness conditions in the ACL2 system was developed. The need for more detailed explanations of the correctness conditions containing the replacement operation rep has led to a change of the algorithms for generating the replacement operation, and the generation of explanations for unproven correctness conditions. Modifications of these algorithms are presented in the article. They allow marking rep definition with semantic labels, extracting semantic labels from rep definition and generating description of break execution condition.

For many years, automotive embedded systems have been validated only by testing. In the near future, Advanced Driver Assistance Systems (ADAS) will take a greater part in the car’s software design and development. Furthermore, their increasing critical level may lead authorities to require a certification for those systems. We think that bringing formal proof in their development can help establishing safety properties and get an efficient certification process. Other industries (e.g. aerospace, railway, nuclear) that produce critical systems requiring certification also took the path of formal verification techniques. One of these techniques is deductive proof. It can give a higher level of confidence in proving critical safety properties and even avoid unit testing.

In this paper, we chose a production use case: a function calculating a square root by linear interpolation. We use deductive proof to prove its correctness and show the limitations we encountered with the off-the-shelf tools. We propose approaches to overcome some limitations of these tools and succeed with the proof. These approaches can be applied to similar problems, which are frequent in the automotive embedded software.

User-friendly formal specifications and verification of parallel and distributed systems from various subject fields, such as automatic control, telecommunications, business processes, are active research topics due to its practical significance. In this paper, we present methods for the development of verification-oriented domain-specific process ontologies which are used to describe parallel and distributed systems of subject fields. One of the advantages of such ontologies is their formal semantics which make possible formal verification of the described systems. Our method is based on the abstract verification-oriented process ontology. We use two methods of specialization of the abstract process ontology. The declarative method uses the specialization of the classes of the original ontology, introduction of new declarative classes, as well as use of new axioms system, which restrict the classes and relations of the abstract ontology. The constructive method uses semantic markup and pattern matching techniques to link sublect fields with classes of the abstract process ontology. We provide detailed ontological specifications for these techniques. Our methods preserve the formal semantics of the original process ontology and, therefore, the possibility of applying formal verification methods to the specialized process ontologies. We show that the constructive method is a refinement of the declarative method. The construction of ontology of the typical elements of automatic control systems illustrates our methods: we develop a declarative description of the classes and restrictions for the specialized ontology in the Prot´eg´e system in the OWL language using the deriving rules written in the SWRL language and we construct the system of semantic markup templates which implements typical elements of automatic control systems.

Property Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases this reasoning is not successful, as invariants should be derived for groups of predicates instead of individual predicates. The article describes a novel algorithm that identifies these groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a up-to-date CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.

We consider the computational implementation of the algorithm for Lyapunov exponents spectrum numerical estimation for delay differential equations. It is known that for such systems, as well as for boundary value problems, it is not possible to prove the well-known Oseledets theorem which allows us to calculate the required parameters very efficiently. Therefore, we can only talk about the estimates of the characteristics in some sense close to the Lyapunov exponents. In this paper, we propose two methods of linearized systems solutions processing. One of them is based on a set of impulse functions, and the other is based on a set of trigonometric functions. We show the usage flexibility of these algorithms in the case of quasi-stable structures when several Lyapunov exponents are close to zero. The developed methods are tested on a logistic equation with a delay, and these tests illustrate the “proximity” of the obtained numerical characteristics and Lyapunov exponents.