JUCS - Journal of Universal Computer Science 9(2): 106-119, doi: 10.3217/jucs-009-02-0106
Checking Object System Designs Incrementally
expand article infoHans-Dieter Ehrich‡, Maik Kollmann‡, Ralf Pinger§
‡ Technical University Braunschweig, Germany§ SIEMENS AG Transportation Systems, Germany

Corresponding author: Hans-Dieter Ehrich ( hd.ehrich@tu-bs.de )

© Hans-Dieter Ehrich, Maik Kollmann, Ralf Pinger.
This article is freely available under the J.UCS Open Content License.
Citation: Ehrich H-D, Kollmann M, Pinger R (2003) Checking Object System Designs Incrementally. JUCS - Journal of Universal Computer Science 9(2): 106-119. https://doi.org/10.3217/jucs-009-02-0106
Open Access
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
multi-object logic, model checking, modelling and design, object system, temporal logic, verification