loading...
Generating Proof Obligation to Verify Object-Z Specification
Tahiti, French Polynesia October 29-November 03
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICSEA.2006.43International Conference on Software ...
 This Article 
 
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Zhicheng Wen, Shanghai University, China
Huaikou Miao, Shanghai University, China
Hongwei Zeng, Shanghai University, China
A formal specification is usable only if it is consistent or non-conflictive. In traditional programming languages, the consistency checking for program is performed at run time. But formal specifications are not executable in general. The syntax parsing and semantics checking in certain tools are not effective for the consistency checking sometimes. Hence, it is difficult to verify the consistency of a formal specification. This paper presents an approach to generating relevant proof obligations for Object-Z specification systemically. It aims to verify the consistency of a specification developed with Object-Z, which enables the specifier to gain confidence. Because Object-Z is an object-oriented formal specification language and has inheritance characteristic, we discuss it from several aspects and take into account the reuse of proof obligation emphatically. Finally, we make use of the theorem prover Z/EVES to analyze and verify the proof obligations.
Index Terms:
Object-Z; formal specification; proof obligation
Citation:
Zhicheng Wen, Huaikou Miao, Hongwei Zeng, "Generating Proof Obligation to Verify Object-Z Specification," icsea, pp.38, International Conference on Software Engineering Advances (ICSEA'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.