Constraint-Oriented Formal Modelling of OO-Systems

Abstract

In addition to static structures, the Unified Modelling Language UML supports the specification of dynamic properties by means of state charts and interaction diagrams. Each diagram, however, only reflects partial aspects of the system. A common behavior model is lacking while it is necessary to relate the diagrams with each other and to enable the verification of dynamic system properties. The formal process specification technique cTLA provides for modular descriptions of behavior constraints and its process composition operation corresponds to superposition. Therefore, a UML diagram can be represented by a cTLA description which is as well modular as it can be combined with the descriptions of other diagrams.