Static analysis techniques to verify mutual exclusion situations within SysML models

Ludovic Apvrille; Pierre De Saqui-Sannes

doi:10.1007/978-3-642-38911-5_6

Static analysis techniques to verify mutual exclusion situations within SysML models

Ludovic Apvrille
, Pierre De Saqui-Sannes

Institut Mines-Télécom
Université Paul Sabatier

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

5 Citations (Scopus)

Résumé

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.

langue originale	Anglais
titre	SDL 2013
Sous-titre	Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings
Pages	91-106
Nombre de pages	16
Les DOIs	https://doi.org/10.1007/978-3-642-38911-5_6
état	Publié - 23 oct. 2013
Modification externe	Oui
Evénement	16th International SDL Forum on Model-Driven Dependability Engineering, SDL 2013 - Montreal, QC, Canada Durée: 26 juin 2013 → 28 juin 2013

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7916 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	16th International SDL Forum on Model-Driven Dependability Engineering, SDL 2013
Pays/Territoire	Canada
La ville	Montreal, QC
période	26/06/13 → 28/06/13

Accès au document

10.1007/978-3-642-38911-5_6

Contient cette citation

Apvrille, L., & De Saqui-Sannes, P. (2013). Static analysis techniques to verify mutual exclusion situations within SysML models. Dans SDL 2013: Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings (p. 91-106). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 7916 LNCS). https://doi.org/10.1007/978-3-642-38911-5_6

Apvrille, Ludovic ; De Saqui-Sannes, Pierre. / Static analysis techniques to verify mutual exclusion situations within SysML models. SDL 2013: Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings. 2013. p. 91-106 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Apvrille, L & De Saqui-Sannes, P 2013, Static analysis techniques to verify mutual exclusion situations within SysML models. Dans SDL 2013: Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 7916 LNCS, p. 91-106, 16th International SDL Forum on Model-Driven Dependability Engineering, SDL 2013, Montreal, QC, Canada, 26/06/13. https://doi.org/10.1007/978-3-642-38911-5_6

Static analysis techniques to verify mutual exclusion situations within SysML models. / Apvrille, Ludovic; De Saqui-Sannes, Pierre.
SDL 2013: Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings. 2013. p. 91-106 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 7916 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Static analysis techniques to verify mutual exclusion situations within SysML models

AU - Apvrille, Ludovic

AU - De Saqui-Sannes, Pierre

PY - 2013/10/23

Y1 - 2013/10/23

N2 - 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.

AB - 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.

KW - Invariants

KW - Model verification

KW - Modeling

KW - Mutual exclusion

KW - Petri Nets

KW - Structural analysis

KW - SysML

U2 - 10.1007/978-3-642-38911-5_6

DO - 10.1007/978-3-642-38911-5_6

M3 - Conference contribution

AN - SCOPUS:84885717314

SN - 9783642389108

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 91

EP - 106

BT - SDL 2013

T2 - 16th International SDL Forum on Model-Driven Dependability Engineering, SDL 2013

Y2 - 26 June 2013 through 28 June 2013

ER -

Apvrille L, De Saqui-Sannes P. Static analysis techniques to verify mutual exclusion situations within SysML models. Dans SDL 2013: Model-Driven Dependability Engineering - 16th International SDL Forum, Proceedings. 2013. p. 91-106. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-38911-5_6

Static analysis techniques to verify mutual exclusion situations within SysML models

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation