TY - GEN
T1 - Towards verifying VDM using SPIN
AU - Lin, Hsin Hung
AU - Omori, Yoichi
AU - Kusakabe, Shigeru
AU - Araki, Keijiro
N1 - Funding Information:
This work was partly supported by KAKENHI, Grant-in-Aid for Scientific Research(S) 24220001.
Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - The Vienna Development Method (VDM) is a formal method that supports modeling and analysis of software systems at various levels of abstraction. Case studies have shown that applying VDM, or formal specification, in general, in software development processes is the key to achieving high-quality software development. However, to derive full benefit from the use of VDM in software development, associative activities such as validating and verifying VDM models are crucial. Since the primary way of verifying a VDM model is specification animation, we aim to utilize the animation feature of VDM to apply model checking techniques. In this paper, we propose an approach to supporting model check VDM models by constructing a hybrid verification model combining VDMJ, a VDM interpreter, and SPIN, one of the most popular model checkers, especially in practical use. Two case studies are reported, and the usability, scalability, and efficiency of our approach are discussed.
AB - The Vienna Development Method (VDM) is a formal method that supports modeling and analysis of software systems at various levels of abstraction. Case studies have shown that applying VDM, or formal specification, in general, in software development processes is the key to achieving high-quality software development. However, to derive full benefit from the use of VDM in software development, associative activities such as validating and verifying VDM models are crucial. Since the primary way of verifying a VDM model is specification animation, we aim to utilize the animation feature of VDM to apply model checking techniques. In this paper, we propose an approach to supporting model check VDM models by constructing a hybrid verification model combining VDMJ, a VDM interpreter, and SPIN, one of the most popular model checkers, especially in practical use. Two case studies are reported, and the usability, scalability, and efficiency of our approach are discussed.
UR - http://www.scopus.com/inward/record.url?scp=84958981964&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958981964&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-29510-7_14
DO - 10.1007/978-3-319-29510-7_14
M3 - Conference contribution
AN - SCOPUS:84958981964
SN - 9783319295091
T3 - Communications in Computer and Information Science
SP - 241
EP - 256
BT - Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
A2 - Ölveczky, Peter Csaba
A2 - Artho, Cyrille
PB - Springer Verlag
T2 - 4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
Y2 - 6 November 2015 through 7 November 2015
ER -