2012 | OriginalPaper | Buchkapitel
On the Formalization of UML Activities for Component-Based Protocol Design Specifications
verfasst von : Prabhu Shankar Kaliappan, Hartmut König
Erschienen in: SOFSEM 2012: Theory and Practice of Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.