Using Formal Methods. A practical comparison between Z/EVES and PVS

Fredholm, Daniel (1997) Using Formal Methods. A practical comparison between Z/EVES and PVS. [SICS Report]



This paper consists of a review and comparison between Z/EVES and PVS--two tools designed for analyzing formal specifications. Z/EVES is a tool for analyzing specifications written in Z. PVS is a general theorem prover for a language that consists of higher order logic together with set theory. The review has its focus on the possibility to use these tools in an industrial context. The plan for the review was to get acquainted with the tools on a general level and then to use them to partially validate a formal specification of requirements for the safety function of railway signaling systems. The conclusion is that PVS is clearly superior to Z/EVES. PVS has such a good performance that it can be recommended for industrial use in the area of formal methods. Concerning Z/EVES, its applicability seems more restricted.

Item Type:SICS Report
Uncontrolled Keywords:formal methods, Z, Z/EVES, PVS, railway signaling
ID Code:2237
Deposited By:Vicki Carleson
Deposited On:28 Jul 2009
Last Modified:09 Feb 2018 10:35

Repository Staff Only: item control page