A Polyadic pi-Calculus Approach for the Formal Specification of UML-RT

Abstract EN

UML-RT is a UML real-time profile that allows modeling event-driven and distributed systems; however it is not a formal specification language.

This paper proposes a formal approach for UML-RT through a mapping of the UML-RT communicating elements into the π-calculus (or pi-calculus) process algebra.

The formal approach both captures the intended behavior of the system being modeled and provides a rigorous and nonambiguous system description.

Our proposal differentiates from other research work because we map UML-RT to π-calculus, and we allow the mapping of dynamic reconfiguration of UML-RT unwired ports.

We illustrate the usage and applicability of the mapping through three examples.

The first example focuses on explaining the mapping; the second one aims to demonstrate the use of the π-calculus definitions to verify system requirements; the third case is an example of mobile processes called Handover protocol.