In software design, UML Statecharts and OCL are used to describe component behaviors and the interactions between components. To verify the design, model checking technology is used and properties are extracted from the software requirements. When composing statecharts directly, the state space explosion problem cannot be avoided. In this paper, we will discuss how to use properties from the software requirements to reduce the statecharts and how the reduction makes it possible to compose statecharts for model checking. To check all properties, different properties are used one by one in the reduction and composition so the verification models contain a set of recuced and composed models to be checked.
Last modified: Tue 2006.07.25 at 09:31 NDT by Dennis Peters