Checking Object System Designs Incrementally
Дата
Авторы
Ehrich,Hans-Dieter
Kollmann,Maik
Pinger,Ralf
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
multi-object logic , model checking , modelling and design , object system , temporal logic , verification