A Methodology for Verifying SysML Requirements using Activity Diagrams

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 https://static-content.springer.com/image/art%3A10.1007%2Fs11334-016-0281-y/MediaObjects/11334_2016_281_IEq1_HTML.gif verify https://static-content.springer.com/image/art%3A10.1007%2Fs11334-016-0281-y/MediaObjects/11334_2016_281_IEq2_HTML.gif 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