Maximilian Odenbrett

 

Explicit-State Model Checking of an Architectural Design Language using SPIN

 

ABSTRACT:

The European Space Agency COMPASS project (Correctness, Modeling, and Performance of Aerospace Systems) aims at the development of a toolset for the coherent application of formal methods to the designing of aerospace systems. I report on an approach to model checking of system models described in (a slight variant of) the Architectural Analysis and Design Language (AADL) by reusing SPIN. To this end, a fully automatic translation tool from automata-like components in AADL to a set of concurrent processes in Promela was developed. This translation involves a fixpoint iteration to solve recursive dependencies between components at run time. Furthermore, a communication protocol is established to allow synchronous communication between more than two components.

To combat the state-space explosion problem in model checking larger systems, abstraction techniques can - or rather: must - be employed. Here, methods that operate on the system specification before constructing its state space are preferable to those that try to minimize the resulting transition system as they generally reduce peak memory requirements. The talk sketches a slicing algorithm for system specifications: Given a specification and a property to be verified, it automatically removes those parts of the specification that are irrelevant for model checking the property, thus reducing the size of the corresponding transition system.

Some experimental results demonstrate the effectiveness of those approaches and conclude the talk.