TY - GEN
T1 - Specifying and checking refinement relationships in VDM++
AU - Kawamata, Yojiro
AU - Sommer, Christian
AU - Ishikawa, Fuyuki
AU - Honiden, Shinichi
PY - 2009/12/1
Y1 - 2009/12/1
N2 - Formal methods allow to verify several properties of specifications and implementations. Intra-specification consistency means that a specification does not contradict itself. When specifications evolve over time, one also wants to check interspecification consistencies, which mean that specifications defined earlier in the development cycle also hold at a later point in time. VDM++ is a popular and easy-to-use formal specification language. It uses testing instead of formal proofs to validate the consistency of specifications. The strictness of validations thus depends on the completeness of the corresponding test suites. Unfortunately, VDM++ does not support the verification of inter-specification consistencies. We define VDM-R, an extension of VDM++, which allows to annotate relationships between specifications. We also provide the tool VR2EvtB to translate from VDM-R to Event-B. Using an Event-B verifier, we can then formally validate intra- and inter-specification consistencies in an almost fully-automated process.
AB - Formal methods allow to verify several properties of specifications and implementations. Intra-specification consistency means that a specification does not contradict itself. When specifications evolve over time, one also wants to check interspecification consistencies, which mean that specifications defined earlier in the development cycle also hold at a later point in time. VDM++ is a popular and easy-to-use formal specification language. It uses testing instead of formal proofs to validate the consistency of specifications. The strictness of validations thus depends on the completeness of the corresponding test suites. Unfortunately, VDM++ does not support the verification of inter-specification consistencies. We define VDM-R, an extension of VDM++, which allows to annotate relationships between specifications. We also provide the tool VR2EvtB to translate from VDM-R to Event-B. Using an Event-B verifier, we can then formally validate intra- and inter-specification consistencies in an almost fully-automated process.
UR - http://www.scopus.com/inward/record.url?scp=77749243208&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77749243208&partnerID=8YFLogxK
U2 - 10.1109/SEFM.2009.34
DO - 10.1109/SEFM.2009.34
M3 - Conference contribution
AN - SCOPUS:77749243208
SN - 9780769538709
T3 - SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
SP - 220
EP - 227
BT - SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
T2 - 7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009
Y2 - 23 November 2009 through 27 November 2009
ER -