An executable formal semantics for UML-RT |
| |
Authors: | Ernesto Posse Juergen Dingel |
| |
Affiliation: | 1.Modelling and Analysis in Software Engineering, School of Computing,Queen’s University,Kingston,Canada |
| |
Abstract: | We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the (pi )-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between “capsules” and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM’s RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|