Sciweavers

Share
SEFM
2005
IEEE

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

12 years 9 months ago
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.
Tarek Sadani, Pierre de Saqui-Sannes, Jean-Pierre
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where SEFM
Authors Tarek Sadani, Pierre de Saqui-Sannes, Jean-Pierre Courtiat
Comments (0)
books