Paper Info
Title
Generating Proof Obligation to Verify Object-Z Specification
Abstract
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.
Year
DOI
Venue
2006
10.1109/ICSEA.2006.43
ICSEA
Keywords
Field
DocType
inheritance characteristic,object-z specification systemically,relevant proof obligation,proof obligation,consistency checking,formal specification,verify object-z specification,syntax parsing,generating proof obligation,certain tool,run time,object-oriented formal specification language,logic,formal verification,object oriented,theorem prover,formal specifications,set theory,computer languages,programming language,programming
Specification language,Programming language,Computer science,Automated theorem proving,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Formal methods,Object-Z,Executable,Formal verification
Conference
ISBN
Citations 
PageRank 
0-7695-2703-5
1
0.35
References 
Authors
6
3
Name
Order
Citations
PageRank
Zhicheng Wen132.16
Huaikou Miao245168.03
Hongwei Zeng34815.44