Sadani, Tarek and Courtiat, Jean-Pierre and Saqui-Sannes, Pierre de From RT-LOTOS to Time Petri Nets new foundations for a verification platform. (2005) In: SEFM'05 - 3rd IEEE International Conference on Software Engineering and Formal Methods, 05-09 Sept 2005, Koblenz, Germany .
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 688kB |
Official URL: http://dx.doi.org/10.1109/SEFM.2005.22
Abstract
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.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
Additional Information: | Thanks to the Institute of Electrical and Electronics Engineers (IEEE). The original PDF can be found on the IEEE website: http://ieeexplore.ieee.org/search/selected.jsp |
Audience (conference): | International conference proceedings |
Uncontrolled Keywords: | |
Institution: | Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) |
Laboratory name: | Département de Mathématiques, Informatique, Automatique - DMIA (Toulouse, France) - Modelisation et Architecture des Systèmes - MARS Laboratoire d'Analyse et d'Architecture des Systèmes - LAAS (Toulouse, France) - Outils Logiciels pour la Communication - OLC |
Statistics: | download |
Deposited On: | 12 Mar 2009 09:40 |
Repository Staff Only: item control page