OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

TEPE: a SysML language for time-constrained property modeling and formal verification

Knorreck, Daniel and Apvrille, Ludovic and Saqui-Sannes, Pierre de TEPE: a SysML language for time-constrained property modeling and formal verification. (2010) In: Third IEEE International workshop UML and Formal Methods - ULM&FM'2010, 16 November 2010 (Shangaï, China).

[img] (Document in English)

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

Official URL: http://dx.doi.org/10.1145/1921532.1921556


Using UML or SysML models in a verification-centric method requires a property expression language, a formal semantics, and a tool. The paper introduces TEPE, a graphical TEmporal Property Expression language based on SysML parametric diagrams. TEPE enriches the expressiveness of other common property languages in particular with the notion of physical time and unordered signal reception. TEPE is further instantiated in the AVATAR real-time UML profile. TTool, an open-source toolkit, implements a press-button approach for the formal verification of AVATAR-TEPE properties with UPPAAL. An elevator system serves as example.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Published in : ACM SIGSOFT Software Engineering Notes, Volume 36, Issue 1, ACM New York, NY, USA. DOI:10.1145/1921532.1921556
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)
Other partners > Télécom Paris (FRANCE)
Laboratory name:
Deposited On:21 Oct 2010 08:44

Repository Staff Only: item control page