OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Real-time and embedded system verification based on formal requirements

Fontan, Benjamin and Apvrille, Ludovic and Saqui-Sannes, Pierre de and Courtiat, Jean-Pierre Real-time and embedded system verification based on formal requirements. (2006) In: IES'06 - Industrial Embedded Systems, 18 October 2006 - 20 October 2006 (Antibes, France).

(Document in English)

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

Official URL: http://dx.doi.org/10.1109/IES.2006.357467


TURTLE is a real-time UML profile supported by a toolkit which enables application of formal verification techniques to the analysis, design and deployment phases of systems design trajectory. This paper extends the TURTLE methodology with a requirement capture phase. SysML requirement diagrams are introduced. Temporal requirements (TR) are formally expressed using a dedicated language based on Allen’s interval algebra. TRs serve as starting point to automatically synthesize observers and to guide the verification process applied to the TURTLE model of the system. Verification results are automatically collected in traceability matrices. A Hybrid Sport Utility Vehicle serves as example.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-04090328
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)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Institut National des Sciences Appliquées de Toulouse - INSA (FRANCE)
Other partners > Télécom Paris (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Laboratory name:
Deposited On:11 Mar 2009 15:40

Repository Staff Only: item control page