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

Download
Author
DeCloss, Daniel P.
Date
2006-06Advisor
Levine, Timothy
Irvine, Cynthia
Metadata
Show full item recordAbstract
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.
Collections
Related items
Showing items related by title, author, creator and subject.
-
Formal models of a least privilege separation kernel in alloy
Phelps, David; Levin, Timothy E.; Auguston, Mikhail (International Conference on i-Warfare and Security, 2008-06-01);We describe the specification of the formal security policy model and formal top-level specification for the Least Privilege Separation Kernel (LPSK) in Alloy, a relatively new modelling language and analysis tool. The ... -
Crowdsourced formal verification: a business case analysis toward a human-centered business model
Baur, Andreas (Monterey, California: Naval Postgraduate School, 2015-06);The DARPA project Crowd Sourced Formal Verification (CSFV) tries to investigate whether offering free games via the Internet that translate player’s actions into program annotations helps to overcome the challenges of the ... -
FNMOC model verification system.
Pace, Kyongsuk P. (Monterey, California. Naval Postgraduate School, 1998-06);Fleet Numerical Meteorology and Oceanography Center (FNMOC) forecasts the atmospheric environment and weather using several meteorological and oceanographic models. These models' forecasting abilities are verified by ...