DocumentCode
2097457
Title
An approach to verify SysML functional requirements using Promela/SPIN
Author
Abdulhameed, Abbas ; Hammad, Ahmed ; Mountassir, Hassan ; Tatibouet, Bruno
Author_Institution
FEMTO-ST Institute, UMR 6174 CNRS, DISC Computer Science Department, University of Franche-Comté France
fYear
2015
fDate
28-30 April 2015
Firstpage
1
Lastpage
9
Abstract
Ensuring the correction of heterogeneous and complex systems is an essential stage in the process of engineering systems. In this paper, we propose an approach to verify and validate complex systems specified by SysML language. We translate SysML specifications into Promela models in order to validate the designed systems by model checking SPIN. The requirements properties are translated to Linear Temporal Logic (LTL) formulae and verified by Spin. A case study is presented to illustrate the effectiveness of our approach.
Keywords
Avatars; Biological system modeling; Model checking; Modeling; Semantics; Unified modeling language; ATL; BDD; Promela; RD; SMD; SPIN; SysML;
fLanguage
English
Publisher
ieee
Conference_Titel
Programming and Systems (ISPS), 2015 12th International Symposium on
Conference_Location
Algiers, Algeria
Type
conf
DOI
10.1109/ISPS.2015.7245003
Filename
7245003
Link To Document