A Polyadic pi-Calculus Approach for the Formal Specification of UML-RT. (7th June 2009) - Bezerra, J. M.; Hirata, C. M.
Abstract : 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.