An Approach to Verify SysML Functional Requirements Using Promela/Spin
| Affiliation auteurs | !!!! Error affiliation !!!! |
| Titre | An Approach to Verify SysML Functional Requirements Using Promela/Spin |
| Type de publication | Conference Paper |
| Year of Publication | 2015 |
| Auteurs | Abdulhameed A, Hammad A, Mountassir H, Tatibouet B |
| Conference Name | 2015 12TH IEEE INTERNATIONAL CONFERENCE ON PROGRAMMING AND SYSTEMS (ISPS) |
| Publisher | IEEE; IEEE Algeria Subsection; USTHB; RSDT; Cerist; SDA; IRIA; MOVEP; BADR Bank; Arpt; CMR; ANVEREDET; Air Algerie |
| Conference Location | 345 E 47TH ST, NEW YORK, NY 10017 USA |
| ISBN Number | 978-1-4799-7700-0 |
| Mots-clés | ATL, BDD, Promela, RD, SMD, SPIN, SysML |
| Résumé | 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. |