Fredholm, Daniel (1997) Using Formal Methods. A practical compairsion 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|
|Deposited By:||Vicki Carleson|
|Deposited On:||28 Jul 2009|
|Last Modified:||18 Nov 2009 16:02|
Repository Staff Only: item control page