Composing Object-Oriented Specifications and Verifications with cTLA
Günter Graw, Peter Herrmann, Heiko Krumm · 1999
In order to support formally correctness preserving refinement steps of objectoriented system designs, we refer at one hand to the practically well-accepted Unified Modelling Language (UML) and at the other hand to L. Lamport's Temporal Logic of Actions (TLA) which supports concise and precise notions of properties of dynamic behaviours and corresponding proof techniques. We apply cTLA which is an extension of TLA and supports the modular definition of process types. Moreover, in cTLA process composition has the character of superposition which facilitates the modular transformation of UML diagrams to corresponding formal cTLA process system definitions and their structured verification. We exemplify transformation and formal verification. Moreover we outline the application of this method for the establishment of domain-specific specification frameworks which can directly support the UML-based correct design of OO-systems.