Related papers: Formal Verification of Control Systems Properties …
In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically…
An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verified by means of a…
Neural network controllers have shown potential in achieving superior performance in feedback control systems. Although a neural network can be trained efficiently using deep and reinforcement learning methods, providing formal guarantees…
A comprehensive verification of parallel software imposes three crucial requirements on the procedure that implements it. Apart from accepting real code as program input and temporal formulae as specification input, the verification should…
In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for…
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows…
Formal Methods are mathematically-based techniques for software design and engineering, which enable the unambiguous description of and reasoning about a system's behaviour. Autonomous systems use software to make decisions without human…
Industrial cyber-physical systems are hybrid systems with strict safety requirements. Despite not having a formal semantics, most of these systems are modeled using Stateflow/Simulink for mainly two reasons: (1) it is easier to model, test,…
Autonomous systems -- such as self-driving cars, autonomous drones, and automated trains -- must come with strong safety guarantees. Over the past decade, techniques based on formal methods have enjoyed some success in providing strong…
We present the concept of a unified graphical environment for expressing the semantics of control systems. The graphical control system design environment in Simulink already allows engineers to insert a variety of assertions aimed the…
We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called…
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for…
Matlab/Simulink is a development and simulation language that is widely used by the Cyber-Physical System (CPS) industry to model dynamical systems. There are two mainstream approaches to verify CPS Simulink models: model testing that…
In this article we present a tool for the verification of programs built on top replicated databases. The tool evaluates a sequential specification and deduces which operations need to be synchronized for the program to function properly in…
A critical step towards certifying safety-critical systems is to check their conformance to hard real-time requirements. A promising way to achieve this is by building the systems from pre-verified components and verifying their correctness…
This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive…
The safety of automated driving systems must be justified by convincing arguments and supported by compelling evidence to persuade certification agencies, regulatory entities, and the general public to allow the systems on public roads.…
Simulink is widely used in industrial design processes to model increasingly complex embedded control systems. Thus, their formal analysis is highly desirable. However, this comes with two major challenges: First, Simulink models often…
Control barrier functions are a popular method of ensuring system safety, and these functions can be used to enforce invariance of a set under the dynamics of a system. A control barrier function must have certain properties, and one must…
Verifying specifications for large-scale control systems is of utmost importance, but can be hard in practice as most formal verification methods can not handle high-dimensional dynamics. Contract theory has been proposed as a modular…