FORMALIZING COLLABORATION-ORIENTED SERVICE SPECIFICATIONS USING TEMPORAL LOGIC
Frank Alexander Kraemer, Peter Herrmann · International Conference on Networking · 2007
In our highly automated engineering approach, reactive services are specified using UML 2.0 collaborations and activities. This enables to focus on complete behaviors between of a set of participants in isolation, and to decompose systems according to the functionalities it should offer. Of course, precise semantics for the specifications are necessary, as we use them as input for model checking and automatic synthesis of components for implementation. For this reason we formalize the concept of collaborations in the temporal logic cTLA by defining the specification style cTLA/c. Collaborations are hereby represented as cTLA processes, and the composition of collaboration can be reduced to process couplings. While cTLA/c is general to capture the semantics of different languages, we show in detail how UML 2.0 activities are mapped to cTLA/c by a set of cTLA processes and production rules.