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
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;
Conference_Titel :
Programming and Systems (ISPS), 2015 12th International Symposium on
Conference_Location :
Algiers, Algeria
DOI :
10.1109/ISPS.2015.7245003
