Verification and Analysis
Many embedded systems are used in safety-critical applications, where errors can endanger human lives and may lead to enormous costs. In contrast to traditional software systems, it is not easily possible to exchanged once delivered software, since users typically have no access to the software of embedded systems. For this reason, the correctness of embedded systems is in many cases of essential importance.
The formal verification of reactive systems is one of the success stories of modern computer science. In particular, model checking methods became 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 verification of temporal properties but also other kinds of analyses.
Each model of computation has certain semantic restrictions that have to be checked to make sure that the system is consistent. For example, for synchronous systems one has to check either the causality (for languages like Quartz and Esterel) or the clock consistency (for languages like Lustre and Signal). Dataflow languages have to implement continuous functions in their processes, and discrete event based systems have to guarantee the absence of deadlocks or live locks in their processes. For these kinds of analyses, formal verification can be applied, and even though these problems are undecidable for general data types, and very complex even for finite data types, there are good heuristics to deal with these problems in practice.
Our Averest systems currently offers model checking of different temporal logics like LTL, CTL and the mu-calculus. To this end, 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 soon available. We also offer translators to NuSMV, a well-known and very efficient symbolic model checker. Moreover, SAT solvers and further decision procedures like the equality logic of uninterpreted functions will also be soon available.
In our recent work, we also consider the problem of temporal logic synthesis, and other kinds of automatic program syntheses. The problem is thereby that one automatically derives an implementation from a declarative specification such that appropriate outputs are determined for all input traces to satisfy the given temporal properties. In particular, we apply these approaches to determine difficult control-flow conditions of programs to avoid e.g. plus/minus one bugs. To this end, we developed efficient determinization procedures for different kinds of omega-automata.
Another recent work deals with the interactive verification of synchronous systems. The ideas is thereby to develop rules of a proof calculus such that proof goals can be decomposed by reducing the system in different ways like program slicing or case splits 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 like Isabelle-HOL.