«

»

Aligning SysML with the B Method to Provide V&V for Systems Engineering

by Erwan Bousse, David Mentré, Benoit Combemale, Benoit Baudry, Katsuragi Takaya
Abstract:
Systems engineering, and especially the modeling of safety critical systems, needs proper means for early Validation and Verification (V&V) to detect critical issues as soon as possible. The objective of our work is to identify a verifiable subset of SysML that is usable by system engineers, while still amenable to automatic transformation towards formal verification tools. As we are interested in proving safety properties expressed using invariants on states, we consider the B method for this purpose. Our approach consists in an alignment of SysML concepts with an identified subset of the B method, using semantic similarities between both languages. We define a restricted SysML extended by a lightweight profile and a transformation towards the B method for V&V purposes. The obtained process is applied to a simplified concrete case study from the railway industry: a SysML model is designed with safety properties, then automatically transformed into B, and finally imported into Atelier-B for automated proof of the properties.
Reference:
Aligning SysML with the B Method to Provide V&V for Systems Engineering (Erwan Bousse, David Mentré, Benoit Combemale, Benoit Baudry, Katsuragi Takaya), In Model-Driven Engineering, Verification, and Validation 2012 (MoDeVVa 2012), workshop at MoDELS’12, 2012.
Bibtex Entry:
@inproceedings{bousse:hal-00741134,
	Abstract = {{Systems engineering, and especially the modeling of safety critical systems, needs proper means for early Validation and Verification (V&V) to detect critical issues as soon as possible. The objective of our work is to identify a verifiable subset of SysML that is usable by system engineers, while still amenable to automatic transformation towards formal verification tools. As we are interested in proving safety properties expressed using invariants on states, we consider the B method for this purpose. Our approach consists in an alignment of SysML concepts with an identified subset of the B method, using semantic similarities between both languages. We define a restricted SysML extended by a lightweight profile and a transformation towards the B method for V&V purposes. The obtained process is applied to a simplified concrete case study from the railway industry: a SysML model is designed with safety properties, then automatically transformed into B, and finally imported into Atelier-B for automated proof of the properties.}},
	Address = {Innsbruck, Austria},
	Author = {Bousse, Erwan and Mentr{'e}, David and Combemale, Benoit and Baudry, Benoit and Takaya, Katsuragi},
	Booktitle = {{Model-Driven Engineering, Verification, and Validation 2012 (MoDeVVa 2012), workshop at MoDELS'12}},
	Month = Sep,
	Pdf = {http://hal.inria.fr/hal-00741134/PDF/paper.pdf},
	Title = {{Aligning SysML with the B Method to Provide V&V for Systems Engineering}},
	Url = {http://hal.inria.fr/hal-00741134},
	Year = {2012},
	Bdsk-Url-1 = {http://hal.inria.fr/hal-00741134}}