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 356kB |
Official URL: https://doi.org/10.1007/978-3-642-38911-5_6
Abstract
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 > Telecom ParisTech (FRANCE) |
Laboratory name: | |
Statistics: | download |
Deposited On: | 22 Apr 2013 13:25 |
Repository Staff Only: item control page