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. © 2013 Springer-Verlag.
CITATION STYLE
Apvrille, L., & De Saqui-Sannes, P. (2013). Static analysis techniques to verify mutual exclusion situations within SysML models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7916 LNCS, pp. 91–106). https://doi.org/10.1007/978-3-642-38911-5_6
Mendeley helps you to discover research relevant for your work.