A Semantics for UML-RT using n-calculus

UML-RT is a UML real-time profile that allows event-driven and distributed systems. UML-RT is not a formal specification language, therefore it is not possible to do formal verification of UML-RT models. This article proposes formal semantics for UML-RT via mapping of UML-RT communicating elements into pi-calculus. The pi-calculus is a process algebra to model concurrent systems. A prototype was also developed; it captures information of UML-RT model from RoseRT and generates pi-calculus definitions according to the proposed mapping rules. The generated pi- calculus definitions use the syntax of HAL-JACK, that is an integrated tool set for the specification, verification and analysis of systems expressed by pi-calculus. In the article, we describe the UML-RT to pi-calculus mapping, we explain the prototype and we present an example of the mapping.