Specifying and checking refinement relationships in VDM++

Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationSEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods
Pages220-227
Number of pages8
DOIs
Publication statusPublished - 2009 Dec 1
Externally publishedYes
Event7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009 - Hanoi, Viet Nam
Duration: 2009 Nov 232009 Nov 27

Other

Other7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009
CountryViet Nam
CityHanoi
Period09/11/2309/11/27

Fingerprint

Specification languages
Specifications
Formal methods

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Science Applications
  • Software

Cite this

Kawamata, Y., Sommer, C., Ishikawa, F., & Honiden, S. (2009). Specifying and checking refinement relationships in VDM++. In SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods (pp. 220-227). [5368087] https://doi.org/10.1109/SEFM.2009.34

Specifying and checking refinement relationships in VDM++. / Kawamata, Yojiro; Sommer, Christian; Ishikawa, Fuyuki; Honiden, Shinichi.

SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods. 2009. p. 220-227 5368087.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kawamata, Y, Sommer, C, Ishikawa, F & Honiden, S 2009, Specifying and checking refinement relationships in VDM++. in SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods., 5368087, pp. 220-227, 7th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Viet Nam, 09/11/23. https://doi.org/10.1109/SEFM.2009.34
Kawamata Y, Sommer C, Ishikawa F, Honiden S. Specifying and checking refinement relationships in VDM++. In SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods. 2009. p. 220-227. 5368087 https://doi.org/10.1109/SEFM.2009.34
Kawamata, Yojiro ; Sommer, Christian ; Ishikawa, Fuyuki ; Honiden, Shinichi. / Specifying and checking refinement relationships in VDM++. SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods. 2009. pp. 220-227
@inproceedings{01a646b6f1264ed1938dfd2fe5d64cab,
title = "Specifying and checking refinement relationships in VDM++",
abstract = "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.",
author = "Yojiro Kawamata and Christian Sommer and Fuyuki Ishikawa and Shinichi Honiden",
year = "2009",
month = "12",
day = "1",
doi = "10.1109/SEFM.2009.34",
language = "English",
isbn = "9780769538709",
pages = "220--227",
booktitle = "SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods",

}

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

SP - 220

EP - 227

BT - SEFM 2009 - 7th IEEE International Conference on Software Engineering and Formal Methods

ER -