UML-RT is a UML real-time profile that allows modeling 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 n-calculus. The p-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 n-calculus definitions according to the proposed mapping rules. The generated n- calculus definitions use the syntax of HAL-JACK, that is an integrated tool set for the specification, verification and analysis of systems expressed by p-calculus. In the article, we describe the UML-RT to n-calculus mapping, we explain the prototype and we present an example of the mapping.
%0 Conference Paper
%1 bezerra_07_semantics
%A Bezerra, Juliana
%A Hirata, Celso M.
%D 2007
%J Rapid System Prototyping, 2007. RSP 2007. 18th IEEE/IFIP International Workshop on
%K _hardcopy 2007 semantics umlrt
%P 75--82
%R 10.1109/RSP.2007.9
%T A Semantics for UML-RT using pi-calculus
%U http://dx.doi.org/10.1109/RSP.2007.9
%X UML-RT is a UML real-time profile that allows modeling 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 n-calculus. The p-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 n-calculus definitions according to the proposed mapping rules. The generated n- calculus definitions use the syntax of HAL-JACK, that is an integrated tool set for the specification, verification and analysis of systems expressed by p-calculus. In the article, we describe the UML-RT to n-calculus mapping, we explain the prototype and we present an example of the mapping.
@inproceedings{bezerra_07_semantics,
abstract = {UML-RT is a UML real-time profile that allows modeling 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 n-calculus. The p-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 n-calculus definitions according to the proposed mapping rules. The generated n- calculus definitions use the syntax of HAL-JACK, that is an integrated tool set for the specification, verification and analysis of systems expressed by p-calculus. In the article, we describe the UML-RT to n-calculus mapping, we explain the prototype and we present an example of the mapping.},
added-at = {2009-02-11T20:48:13.000+0100},
author = {Bezerra, Juliana and Hirata, Celso M.},
biburl = {https://www.bibsonomy.org/bibtex/2d5cbe8268b87139e306c8cf91f3b2586/leonardo},
citeulike-article-id = {1402781},
doi = {10.1109/RSP.2007.9},
interhash = {00141d89cc90c1e01b8d5855d144873f},
intrahash = {d5cbe8268b87139e306c8cf91f3b2586},
journal = {Rapid System Prototyping, 2007. RSP 2007. 18th IEEE/IFIP International Workshop on},
keywords = {_hardcopy 2007 semantics umlrt},
pages = {75--82},
posted-at = {2007-06-21 18:07:45},
priority = {4},
timestamp = {2009-02-11T20:48:13.000+0100},
title = {A Semantics for UML-RT using pi-calculus},
url = {http://dx.doi.org/10.1109/RSP.2007.9},
year = 2007
}