OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Static analysis techniques to verify mutual exclusion situations within SysML models

Apvrille, Ludovic and Saqui-Sannes, Pierre de Static analysis techniques to verify mutual exclusion situations within SysML models. (2013) In: SDL 2013 - 16th International System Design Languages Forum, 26 June 2013 - 28 June 2013 (Montreal, Canada).

(Document in English)

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

Official URL: https://doi.org/10.1007/978-3-642-38911-5_6


AVATAR is a real-time extension of SysML supported by the TTool open-source toolkit. So far, formal verification of AVATAR models has relied on reachability techniques that face a state explosion problem. The paper explores a new avenue: applying structural analysis to AVATAR model, so as to identify mutual exclusion situations. In practice, TTool translates a subset of an AVATAR model into a Petri net and solves an equation system built upon the incidence matrix of the net. TTool implements a push-button approach and displays verification results at the AVATAR model level. The approach is not restricted to AVATAR and may be adapted to other UML profiles.

Item Type:Conference or Workshop Item (Paper)
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
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:22 Apr 2013 13:25

Repository Staff Only: item control page