Abstract

Software Model Checking

Prof. Leue

As the complexity of embedded software systems is increasing at a tremendous pace, convincing oneself that these systems are doing what they are supposed to do is an important step in assuring these systems' safe operation. Model checking has recently enjoyed increasing interest in the software engineering community. Complementing classical verification and software quality assurance techniques such as testing and code reviews, model checking offers an automated and systematic way to exhaustively explore the state space of the model of a software system. In doing so, the model checker searches for states or state sequences violating a given property specification. If such a property violation exists, the model checker will produce an offending sequence of execution steps, called counterexample, which aids in explaining the cause of the property violation. Model checking is a terminating procedure, if the state space is of finite size. It can be automated, i.e., once the software model has been built and the property of interest has been specified, no more user interaction is required. These properties make it easy to seamlessly integrate model checking technology into industrial software design processes.

The objective of this presentations is to introduce participants into the main ideas underlying model checking as it is applied to the analysis of software systems. We will review the main model checking technologies and introduce into explicit state model checking, illustrated using the public domain model checking tool SPIN (http://spinroot.com). We will illustrate some classical applications of this technology where the analysis is based on a preceding modeling step. We will finally describe the state of the art and the main challenges in software model checking, which aims at the direct analysis of embedded software code avoiding an intervening modeling step.

Zurück