On the Formalization of UML Activities for Component-Based Protocol Design Specifications

Formal description techniques, such as LOTOS and SDL, have been proven as a successful means for developing communication protocols and distributed systems. Meanwhile the Unified Modeling Language (UML) has achieved wide acceptance. It is, however, less applied in the field of protocol design due to the lack of an appropriate formal semantics. In this paper we propose a formalization technique for UML activity diagrams using the compositional Temporal Logic of Actions (cTLA). We use cTLA because it can express correctness properties in temporal logic and can also be verified formally using several model checking mechanisms. The approach consists of two steps. First, we predefine the formal semantics of the most commonly used UML activity nodes using simple cTLA. In the second step we derive the functional semantics of the activity diagram by mapping it to a compositional cTLA process. We illustrate our approach for a connection set up as an example. Finally we present with the Activity to cTLA generator a tool to automate this process.