@inproceedings{5590cb9ac4ec4733bfb08b838598939c,
title = "Static analysis techniques to verify mutual exclusion situations within SysML models",
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 models, 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.",
keywords = "Invariants, Model verification, Modeling, Mutual exclusion, Petri Nets, Structural analysis, SysML",
author = "Ludovic Apvrille and \{De Saqui-Sannes\}, Pierre",
year = "2013",
month = oct,
day = "23",
doi = "10.1007/978-3-642-38911-5\_6",
language = "English",
isbn = "9783642389108",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "91--106",
booktitle = "SDL 2013",
note = "16th International SDL Forum on Model-Driven Dependability Engineering, SDL 2013 ; Conference date: 26-06-2013 Through 28-06-2013",
}