A Semantics for UML-RT using n-calculus

Author

de Melo Bezerra, Juliana ; Hirata, Celso Massaki

Author_Institution

Inst. Tecnologico de Aerondutica, Sao Paolo

fYear

2007

fDate

28-30 May 2007

Firstpage

75

Lastpage

82

Abstract

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.

Keywords

Unified Modeling Language; formal specification; formal verification; pi calculus; programming language semantics; real-time systems; HAL-JACK syntax; RoseRT; UML real-time; UML-RT formal semantics; Unified Modeling Language; distributed system modeling; event-driven modeling; formal specification; formal verification; pi-calculus process algebra; Algebra; Calculus; Carbon capture and storage; Computer science; Formal specifications; Formal verification; Logic; Prototypes; Real time systems; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Rapid System Prototyping, 2007. RSP 2007. 18th IEEE/IFIP International Workshop on

Conference_Location

Porto Alegre

ISSN

1074-6005

Print_ISBN

0-7695-2834-1

Type

conf

DOI

10.1109/RSP.2007.9

Filename

4228489