A Case Study on the Application of PVS to Requirements Analysis

<body> <table width="100%"> <tr> <td align="center"> This page requires frames. <a href="http://dl.acs.org.au/index.php/ajis/article/viewPDFInterstitial/298/268">Click here</a> for the non-frames version. <p>Non-frames version <a href="http://dl.acs.org.au/index.php/ajis/article/viewPDFInterstitial/298/268">available</a>.</p> </td> </tr> </table> <h1>A Case Study on the Application of PVS to Requirements Analysis</h1> <h2><i>Georg Droschl</i></h2> <h3>Australasian Journal of Information Systems</h3> <h4>Abstract</h4> <div>This paper presents the results of a formal methods case study in which the Prototype Verification System (PVS) has been used for requirements analysis of one module of a physical access control system. PVS is a tool for writing formal specifications and constructing proofs. Previously, the same requirements have been analyzed by means of testing supported by the IFAD Toolbox for VDM-SL. The capabilities of the two formal methods are compared.</div> </body>