Checking Object System Designs Incrementally

Hans-Dieter Ehrich (Technical University Braunschweig, Germany)

Maik Kollmann (Technical University Braunschweig, Germany)

Ralf Pinger (SIEMENS AG Transportation Systems, Germany)

Abstract: We present a method for checking global conditions for object systems in a way that avoids state space explosion. The objects referred to in a global condition are checked step by step against local conditions and communication requirements derived from the global condition. The derivation is automatic, based on information about the system structure contained in the global condition. The approach is demonstrated using model checking, but the idea works for other approaches to verification or testing as well. In our current investigation, a multi-object variant of CTL is used for expressing global conditions. The local conditions and communication requirements can be verified independently using standard model checkers. The method is illustrated by a large example (about 10 24 states) where our method shows a spectacular speedup over global model checking.

Keywords: model checking, modelling and design, multi-object logic, object system, temporal logic, verification

Categories: F.3.1, I.6.4