Model checking embedded system designs

Model checking has established itself as a successful tool supported technique for the verification and debugging of various hardware and software systems [16]. Not only in academia, but also by industry this technique is increasingly being regarded as a promising and practical proposition, especially in the area of hardware verification [22]. Model checking is also being applied with success to the analysis of the control software in embedded systems [37]. Because such systems are often mission critical, in the sense that their failure to operate correctly can be very costly in terms of cost and safety, there is a natural tendency to apply advanced methods to guide and analyse their design. Because model checkers typically trace the behaviour leading to the explored states they can be used not only analytically, i.e. to verify that given control designs are correct, but also synthetically, i.e. to derive or optimize control designs. Examples of such controller synthesis in the context of timed automata can be found in [31, 7]. In this extended abstract we survey the basic principles behind the application of model checking to controller verification and synthesis. Although the development of model checkers for sophisticated models of system behaviour is a nontrivial task, the conceptual ingredients often remain straightforward. The major problem besetting model checking, as with many tools dealing with concurrent systems, is the infamous state space explosion, caused by the fact that the global state space of a system grows exponentially with the local state spaces of its components. The more sophisticated the model of behaviour, the more difficult to control this phenomenon effectively. This makes abstract modelling and state space search techniques decisive practical ingredients of model checking applications, more than the sophistication of the behavioural model that is supported. A promising development is the area of guided model checking, in which the state space search strategy of the model checking algorithm can be influenced to visit more interesting sets of states first. In particular, we will discuss how model checking can be combined with heuristic cost functions to guide search strategies. In the final section of this extended abstract we list a number of current research developments, especially in the area of reachability analysis for optimal control and related issues.