Verification and Analysis

Many embedded systems are used in safety-critical applications where errors can endanger lives and result in enormous costs. Unlike traditional software systems, once software is delivered, it cannot be easily replaced because users typically do not have access to the software of embedded systems. For this reason, the correctness of embedded systems is critical in many cases.

Formal verification of reactive systems is one of the success stories of modern computer science. In particular, model checking methods have become efficient enough to be useful for practical examples. Advances in symbolic model checking, partial order reduction, symmetry reduction, and other abstraction techniques are key techniques not only for verifying temporal properties, but also for other types of analysis.

Each computational model has certain semantic constraints that must be checked to ensure that the system is consistent. For example, synchronous systems need to check either causality (for languages like Quartz and Esterel) or clock consistency (for languages like Lustre and Signal). Dataflow languages need to implement continuous functions in their processes, and discrete event-based systems need to guarantee the absence of deadlocks or live locks in their processes. For these kinds of analyses, formal verification can be applied, and while these problems are undecidable for general data types, and very complex even for finite data types, there are good heuristics for dealing with them in practice.

Our Averest system currently provides model checking for various temporal logics such as LTL, CTL, and the mu-calculus. For this purpose, several translations from temporal logics to omega automata and the mu-calculus have been implemented, and a symbolic model checker for the vector mu-calculus will be available soon. We also provide compilers for NuSMV, a well-known and very efficient symbolic model checker. In addition, SAT solvers and other decision procedures such as the equality logic of uninterpreted functions will be available soon.

In our recent work, we also consider the problem of temporal logic synthesis and other types of automatic program synthesis. The problem is to automatically derive an implementation from a declarative specification in such a way that, for all input traces, appropriate outputs are determined to satisfy the given temporal properties. In particular, we apply these approaches to determine difficult control flow conditions of programs, e.g. to avoid plus/minus one bugs. To this end, we have developed efficient determinization procedures for different types of omega automata.

Another recent work deals with interactive verification of synchronous systems. The idea is to develop rules of a proof calculus such that proof goals can be decomposed by reducing the system in various ways, such as program slicing or case splitting by control flow locations or boolean conditions on variables. In particular, the result is a specialized theorem prover with an infrastructure that follows interactive theorem provers for higher-order logic such as Isabelle-HOL.

References

			[GrVe08] O. Grumberg and H. Veith 25 Years of Model Checking -- History, Achievements, Perspectives
			[KeGr99] C. Kern and M.R. Greenstreet Formal Verification in Hardware Design: A Survey ACM Transactions on Design Automation of Electronic Systems (TODAES)
			[Gupt92] A. Gupta Formal Hardware Verification Methods: A Survey Formal Methods in System Design (FMSD)
			[Schn03] K. Schneider Verification of Reactive Systems -- Formal Methods and Algorithms Springer
			[ClGP99] E.M. Clarke and O. Grumberg and D.A. Peled Model Checking MIT Press