loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 Seventh IEEE International Conference on Software Engineering and Formal Methods
Specifying and Checking Refinement Relationships in VDM++
Hanoi, Vietnam
November 23-November 27
ISBN: 978-0-7695-3870-9
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 inter-specification 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.
Citation:
Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa, Shinichi Honiden, "Specifying and Checking Refinement Relationships in VDM++," sefm, pp.220-227, 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009
Usage of this product signifies your acceptance of the Terms of Use.