Return to search

An analysis of Specware and its usefulness in the verification of high assurance systems

Formal verification is required for systems that require high assurance. Formal verification can require large and complex proofs that can drastically affect the development life cycle. Through the use of a verification system, such proofs can be managed and completed in an efficient manner. A verification system consists of a specification language that can express formal logic, and an automated theorem tool that can be used to verify theorems and conjectures within the specifications. One example of a verification system is Specware. This thesis presents an analysis of Specware against a set of evaluation criteria in order to determine the level of usefulness Specware can have in the verification of high assurance systems. This analysis revealed that Specware contains a powerful specification language capable of representing higher order logic in a simple and expressive manner. Specware is able to represent multiple levels of abstraction and generate proof obligations regarding specification correctness and interlevel mapping. The theorem prover associated with Specware was found to be lacking in capability. Through this analysis we found that Specware has great potential to be an excellent verification system given improvement upon the theorem prover and strengthening of weaknesses regarding linguistic components. / Naval Postgraduate School author (civilian).

Identiferoai:union.ndltd.org:nps.edu/oai:calhoun.nps.edu:10945/2764
Date06 1900
CreatorsDeCloss, Daniel P.
ContributorsLevine, Timothy, Irvine, Cynthia, Naval Postgraduate School (U.S.), Computer Science
PublisherMonterey, California. Naval Postgraduate School
Source SetsNaval Postgraduate School
Detected LanguageEnglish
TypeThesis
Formatxiv, 95 p. : ill., 1 table ;, application/pdf
RightsApproved for public release, distribution unlimited

Page generated in 0.0017 seconds