–
Room P3.10, Mathematics Building
Checking object system designs
A method is presented for checking global conditions for object system designs by checking the object models concerned, i.e. referred to in the condition, and their mutual communication requirements. The method deals with one object at a time, thus avoiding state space explosion. The approach is demonstrated using model checking, but the idea works for other approaches to verification or testing as well. A multi-object variant of CTL is used for expressing global conditions, making the system structure sufficiently visible to enable automatic translation into local conditions for the objects concerned, and for the communication requirements among them. The former as well as the latter can be verified independently using standard model checkers. The method is illustrated by a large example where our method shows a spectacular speedup over global model checking.