OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formal and efficient verification techniques for Real-Time UML models

Sadani, Tarek and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Formal and efficient verification techniques for Real-Time UML models. (2006) In: ERTS'06 - 3rd European Congress ERTS Embedded Real Time Software, 25-27 Janv 2006, Toulouse, France .

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
459Kb

Official URL: http://www.sia.fr/dyn/publications_detail.asp?codepublication=R-2006-01-3B1

Abstract

The real-time UML profile TURTLE has a formal semantics expressed by translation into a timed process algebra: RT-LOTOS. RTL, the formal verification tool developed for RT-LOTOS, was first used to check TURTLE models against design errors. This paper opens new avenues for TURTLE model verification. It shows how recent work on translating RT-LOTOS specifications into Time Petri net model may be applied to TURTLE. RT-LOTOS to TPN translation patterns are presented. Their formal proof is the subject of another paper. These patterns have been implemented in a RT-LOTOS to TPN translator which has been interfaced with TINA, a Time Petri Net Analyzer which implements several reachability analysis procedures depending on the class of property to be verified. The paper illustrates the benefits of the TURTLE->RT-LOTOS->TPN transformation chain on an avionic case study.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Société des ingénieurs de l'automobile. The definnitive version is available at : http://www.sia.fr/dyn/publications_detail.asp?codepublication=R-2006-01-3B1
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE
French research institutions > Centre National de la Recherche Scientifique - CNRS
Laboratory name:
Statistics:download
Deposited By:Pierre de Saqui-Sannes

Repository Staff Only: item control page