TURTLE-P: A UML profile for the formal validation of critical and distributed systems. The timed UML and RT-LOTOS environment, or TURTLE for short, extends UML class and activity diagrams with composition and temporal operators. TURTLE is a real-time UML profile with a formal semantics expressed in RT-LOTOS. Further, it is supported by a formal validation toolkit. This paper introduces TURTLE-P, an extended profile no longer restricted to the abstract modeling of distributed systems. Indeed, TURTLE-P addresses the concrete descriptions of communication architectures, including quality of service parameters (delay, jitter, etc.). This new profile enables co-design of hardware and software components with extended UML component and deployment diagrams. Properties of these diagrams can be evaluated and/or validated thanks to the formal semantics given in RT-LOTOS. The application of TURTLE-P is illustrated with a telecommunication satellite system.
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Bianco, Vieri del; Lavazza, Luigi; Mauri, Marco; Occorso, Giuseppe: Towards uML-based formal specifications of component-based real-time software (2007)
- Apvrille, Ludovic; De Saqui-Sannes, Pierre; Khendek, Ferhat: TURTLE-P: A UML profile for the formal validation of critical and distributed systems (2006)
- Sadani, Tarek; Boyer, Marc; de Saqui-Sannes, Pierre; Courtiat, Jean-Pierre: Effective representation of RT-LOTOS terms by finite time Petri nets (2006)
- Apvrille, Ludovic; Courtiat, Jean-Pierre; Lohr, Christophe; de Saqui-Sannes, Pierre: TURTLE: A Real-Time UML Profile Supported by a Formal Validation Toolkit (2004)
- Del Bianco, Vieri; Lavazza, Luigi; Mauri, Marco; Occorso, Giuseppe: Towards UML-based formal specifications of component-based real-time software (2003)