We present an efficient method for verifying global conditions for (large) distributed object systems using conventional model checkers. Global conditions are expressed in a distributed variant of CTL, making the distribution structure sufficiently visible to enable automatic translation into local conditions for the single objects and for the communication between them. These can be verified one after the other or parallel using existing model checkers. Our method avoids state space explosion if the amount of communication traffic between objects is limited. It is illustrated by a large example where our method shows a dramatic speedup and improvements in practicability over conventional model checking.
|