Affiliations: College of Computer Science, Jiangxi University of Engineering, Xinyu, Jiangxi, China
Correspondence:
[*]
Corresponding author: Zhicheng Wen, College of Computer Science, Jiangxi University of Engineering, Xinyu, Jiangxi, China. Tel.: +86 15873372746; E-mail: zcwen@mail.shu.edu.cn.
Abstract: A software formal specification is useful if and only if it is consistent or non-conflictive. However, checking the correctness or consistency of a formal specification is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs. Checking the correctness and consistency of Object-Z formal specification is the main goal, which can make the specifier to get confident. Because Object-Z has inheritance property, this paper discusses it from different aspects, and focuses on the reuse of theorem proof. Finally, theorem prover Z/EVES is used to analyze and verify the Object-Z theorem proofs (semi-)automatically.
Keywords: Object-Z, elevator system, formal specification, Z/EVES, theorem proof
