A methodology for verifying SysML requirements using activity diagrams. (March 2017)

• Record Type: Journal Article
• Authors: Rahim, Messaoud; Hammad, Ahmed; Ioualalen, Malika
• Is Part Of: Innovations in systems and software engineering. Volume 13:Number 1(2017)
• Page Start: 19
• Page End: 33
• Publication Date: 2017-03
• Subjects: SysML -- Activity diagram -- Requirement diagram -- Requirements formalization -- Verification -- Model-checking -- Hierarchical coloured Petri nets; Software engineering -- Periodicals; Systems engineering -- Periodicals; Génie logiciel -- Périodiques; Ingénierie des systèmes -- Périodiques; Electronic journals; 005.1
• DOI: 10.1007/s11334-016-0281-y
• Languages: English
• ISSNs: 1614-5046

Abstract

Abstract Designing complex and critical systems needs a methodology to ensure the correctness of their specifications. Within an overall approach which considers the validation of SysML designs, this paper proposes a methodology for verifying SysML requirements on activity diagrams. The objective is to define a complete process to formalize and verify SysML functional requirements related to activity diagrams. Our contributions lie, first, in the definition of AcTRL (Activity Temporal Requirement Language), a new language for the formalization of functional requirements at SysML level. Second, in the proposed verification methodology which is guided by the verify relationships between SysML requirements and activity diagrams. The verification is enabled by formalizing SysML activities with hierarchical coloured Petri nets (HCPNs) and by automatically translating SysML requirements expressed on AcTRL into temporal logic. Our methodology takes into account the hierarchical structure of SysML activities and their relations with SysML requirements to provide a modular and incremental verification. A case study for a ticket vending machine is presented to illustrate the different steps and the benefits of the proposed methodology.