We investigate the formal verification of the control software of critical systems, i.e., the verification of the compliance of the designed system with th

KeYmaera is an interactive theorem prover and is used to verify safety properties of cyber-physical systems (CPSs). It implements a Dynamic Logic for Hybrid Programs (HPs), while a HP models a CPS very precisely. Verifying properties of a given system in KeYmaera can become a challenge for a user since the proof is authored in a classical sequent calculus framework and a successful proof requires from the user intimate knowledge of the available calculus rules. Another barrier for widespread application of KeYmaera is the purely textual representation of current proof goals, what requires from the user very good training, experience, and patience. In this paper, we present an alternative verification approach based on KeYmaera, which drastically improves usability and minimizes user interaction. The main idea is to let the user annotate invariants and contracts to states of the hybrid automaton. Thus, the user can employ the graphical representation of the modelled system and is not bound to the purely textual form of hybrid programs as in KeYmaera. Based on the user-provided contracts, one can generate proof obligations, which are much simpler than the original proof goal in KeYmaera. The article is published in the authors’ wording.

The work is devoted to the research that was carried out within the framework of computer vision problems applicable to the analysis of images and video information with vehicles. We solve the problem of classifying vehicles. We analyze the drawbacks of Haar features and convolutional neural networks and test the obtained networks using the key point method; we construct an integral algorithm that includes several networks, and we further validate it on a large number of real photographs and types of vehicles. Next, we solve the task to develop a software framework for tracking vehicles by analyzing adjacent photographs from a video sequence. After that, we consider the tracking task in more detail. We analyze modern tracking algorithms using machine learning and describe our implemented tracker with support for the appearance of obstacles between the camera and a moving vehicle. As a result, we propose algorithms and open-source software that, after being configured for specific cameras, can be used in traffic analysis systems.

The paper proposes a topology-free specification of distributed control systems by means of a process-oriented programming paradigm. The proposed approach was characterized, on the one hand, by a topologically independent specification of the control algorithm and, on the other hand, by the possibility of using existing formal verification methods by preserving the semantics of a centralized process-oriented program. The paper discusses the advantages of a topologically independent specification of distributed control systems, outlines the features of control software, argues why the use of a process-oriented approach to the development of the automation of cyber-physical systems is suitable for solving these problems, describes a general scheme for implementing a distributed control system according to a process-oriented specification, and proposes a formal heuristic algorithm for partitioning a sequential process-oriented program into independent clusters. We illustrate our algorithm with bottle-filling and sluice case studies.

Currently, requirements for control software written in natural language are often formulated ambiguously and incompletely. Controlled natural languages (CNLs) can solve this problem, at the same time maintaining flexibility for writing and conveying requirements in an intuitive and common way. The creation of domain-specific controlled natural languages nowadays is under active development. In this paper, we suggest CNL which is based on event-driven semantics. This language is intended for describing the temporal properties of cyber-physical systems. We develop our CNL using a number of natural language patterns build for classes of requirements expressed in Event-Driven Temporal Logic formalism (EDTL). Due to formal semantics of EDTL, the suggested CNL is also unambiguous and can be translated into logic formulas. As a result, the proposed CNL provides an auxiliary tool to improve communication quality between different participants in the industrial system development process: customers, requirements engineers, developers, and others. Therefore, the solution helps to reduce the number of errors in the formulation of requirements at earlier stages of development.