Formal verification of sequence diagram using DiVinE

摘要

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.