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.
SmithG., The Object-Z Specification Language, Advances in Formal Methods, Kluwer Academic Publishers, 2000.
2.
WoodcockJ. and DaviesJ., Using Z: Specification, Proof and Refinement, Prentice Hall International Series in Computer Science, 1996.
3.
LiuM.MaW.DengS. et al., Modeling and verification of services oriented cyber physical systems, Journal of Computer Applications34(6) (2014), 1770–1773.
4.
HouG.ZhouK.ChangJ. and WangJ., Software formal modeling and verification method based on time STM, Journal of Software26(2) (2015), 223–238.
5.
GuidottiD.LeofanteF. and TacchellaA., Improving reliability of myocontrol using Formal Verification, IEEE Transactions on Neural Systems and Rehabilitation Engineering27(4) (2019), 564–571.
6.
MaL.LiW.LiangC. and LiA., Formal modeling and verification of resource-oriented internet of things systems, Journal of Chinese Computer Systems39(1) (2018), 140–145.
7.
MeiselsI. and SaaltinkM., The Z/EVES 2.0 reference manual, ORA Canada, 1999.
8.
FreitasL. and WoodcockJ., Checking the CICS file control API with Z/EVES: an experiment in the verified software repository, Science of Computer Programming74(4) (2009), 197–218.
9.
RibeiroA. and LarsenP.G., Theorem proof generation and discharging for recursive definitions in VDM, Formal Methods and Software Engineering (2010), 40–55.
10.
KatzS. and RashidA., From aspectual requirements to theorem proofs for aspect-oriented systems, in: 12th IEEE International (RE’04), 2004, pp, 48–57.
11.
HallerstedeS., On the purpose of Event-B theorem proofs, Abstract State Machines, B and Z (2008), 125–138.
12.
ZhangY. and DuanF., Formal transformation and verification of UML model based on specification Z, Computer Engineering and Design34(6) (2013), 2031–2035.
13.
XuQ.MiaoH.CaoX. and HuX., Automatic test case generator for Object-Z specification, Journal of Software22(6) (2011), 1155–1168.
14.
DongY. and GaoX., Method for generating formal interlocking software model based on scenario, Computer Science42(1) (2015), 193–195+226.
