From RT-LOTOS to Time Petri Nets New Foundations for a Verification Platform

The formal description technique RT-LOTOS has been selected as intermediate language to add formality to a real-time UML profile named TURTLE. For this sake, an RT-LOTOS verification platform has been developed for early detection of design errors in real-time system models. The paper discusses an extension of the platform by inclusion of verification tools developed for Time Petri Nets. The starting point is the definition of RT-LOTOS to TPN translation patterns. In particular, we introduce the concept of components embedding Time Petri Nets. The translation patterns are implemented in a prototype tool which takes as input an RT-LOTOS specification and outputs a TPN in the format admitted by the TINA tool. The efficiency of the proposed solution has been demonstrated on various case studies.

• Type: Conference
• Year: 2005
• Where: SEFM
• Authors: Tarek Sadani, Pierre de Saqui-Sannes, Jean-Pierre Courtiat
• Keywords: RT-LOTOS Verification Platform, SEFM 2005, Software Engineering, Time Petri Nets, Translation Patterns