Abstract:

Embedded control software is ubiquitous nowadays. It is a significant component of, for instance, home appliances, cars, and medical devices. As the uses of software increase in our daily life, the importance of its correctness increases as well. At the same time, expectations for embedded control software are usually higher than for desktop applications, making correctness a crucial problem in this domain.

One approach to improve the reliability of embedded control software is by means of validation and verification techniques, which analyze a system and try to determine if the given requirements are satisfied. Techniques like numerical simulation check that the system behaves correctly by exploring a number of its possible behaviors. Techniques like model checking, on the other hand, formally establish the validity of properties of the system.

The focus of this thesis is the combination of software model checking with numerical simulation for validation and verification of embedded control software. A characteristic of embedded control software is the interaction with an environment that is continuous in nature. This makes model checking more difficult as the system has an infinite number of states.

This thesis aims at developing different techniques that can be used to analyze control systems. These techniques range from an optimized version of numerical simulation to a conservative approach for the verification of control system's safety. The techniques not only differ in the type of results they can provide (correctness versus bug finding), but also in the associated complexity. I see these approaches as a first step toward developing a spectrum of techniques with different costs that can be applied to analyze control systems.

In this proposal, I first describe an approach called systematic simulation that employs a model checker to explore the behaviors of a software implementation while using MATLAB/Simulink to model and simulate the continuous environment. This approach is used to perform bounded-time verification of an embedded control system with a finite set of initial states whose controller is implemented in software. Next, I present an approach based on a notion of approximate equivalence between states of the systems that can be used to test an embedded control system by determining during the analysis which traces to explore. Last, I present a conservative extension of the latter approach that is able to formally verify bounded-time safety of embedded control software. This approach performs a conservative merging of traces that are similar, based on a conservative notion of equivalence between states. So far I have applied these techniques to a few control system examples including the design of an unmanned aerial vehicle (UAV) based on the Stanford Testbed of Autonomous Rotorcraft for Multi-Agent Control (STARMAC).