Using Formal Methods. A practical compairsion between Z/EVES and PVS
Number of Authors: 1
1997 (English)Report (Refereed)
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.
Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1997, 1. , 24 p.
SICS Technical Report, ISSN 1100-3154 ; T97:04
formal methods, Z, Z/EVES, PVS, railway signaling
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-14150OAI: oai:DiVA.org:ri-14150DiVA: diva2:1035437