DocumentCode
263956
Title
Formal verification of sequence diagram using DiVinE
Author
Basit-Ur-Rahim, Muhammad Abdul ; Arif, Fahim ; Ahmad, Jawad
Author_Institution
Mil. Coll. of Signals, Nat. Univ. of Sci. & Technol., Rawalpindi, Pakistan
fYear
2014
fDate
17-19 Jan. 2014
Firstpage
1
Lastpage
6
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.
Keywords
formal verification; parallel processing; specification languages; DVE; DiVinE parallel model checking tool; SysML; formal verification; graphical modeling language; graphical models; modeling cost; semiformal language; sequence diagram; system development cycles; system engineering applications; system modeling language; verification cost; Educational institutions; Model checking; Radiation detectors; Reliability; Software; Synchronization; Unified modeling language; DiVinE; Parallel model checking; Sequence Diagram; SysML; Verification and validation;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Applications and Information Systems (WCCAIS), 2014 World Congress on
Conference_Location
Hammamet
Print_ISBN
978-1-4799-3350-1
Type
conf
DOI
10.1109/WCCAIS.2014.6916659
Filename
6916659
Link To Document