Formal verification of sequence diagram using DiVinE
Muhammad Abdul Basit Ur Rahim, Fahim Arif, Jamil Ahmad
Abstract
Muhammad Abdul Basit Ur Rahim, Fahim Arif, Jamil Ahmad
Abstract
System modeling language is used to model the system engineering applications. This graphical modeling language is a semi-formal language. To develop a reliable application, the graphical models for large scale critical and complex applications must be validated and verified against user requirements in earlier phase of system development cycles. The sequence diagram is one of the popular diagram of SysML. The fragments of sequence diagram increase its functionality but the complexity as well. In this paper, a methodology is proposed to verify the sequence diagram including its fragments. The verification is performed using DiVinE parallel model checking tool that not only accelerates verification speed but also save modeling and verification cost. The rules have been specified to translate these individual fragments to DiVinE's supported language DVE. To develop a reliable product, our results suggest the use of DiVinE for verification of sequence diagram including its fragments.
OpenAlex reports 5 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
System modeling language is used to model the system engineering applications. This graphical modeling language is a semi-formal language. To develop a reliable application, the graphical models for large scale critical and complex applications must be validated and verified against user requirements in earlier phase of system development cycles. The sequence diagram is one of the popular diagram of SysML. The fragments of sequence diagram increase its functionality but the complexity as well. In this paper, a methodology is proposed to verify the sequence diagram including its fragments. The verification is performed using DiVinE parallel model checking tool that not only accelerates verification speed but also save modeling and verification cost. The rules have been specified to translate these individual fragments to DiVinE's supported language DVE. To develop a reliable product, our results suggest the use of DiVinE for verification of sequence diagram including its fragments.
Key concepts: Systems Modeling Language, Sequence diagram, Computer science, Communication diagram, Sequence (biology), Programming language, Diagram, Class diagram