File:An analysis of Specware and its usefulness in the verification of high assurance systems (IA annalysisofspecw109452764).pdf
Original file (1,275 × 1,650 pixels, file size: 472 KB, MIME type: application/pdf, 112 pages)
Captions
Captions
Summary
[edit]An analysis of Specware and its usefulness in the verification of high assurance systems
(   ) |
||
|---|---|---|
| Author |
DeCloss, Daniel P. |
 |
| Title |
An analysis of Specware and its usefulness in the verification of high assurance systems |
|
| Publisher |
Monterey, California. Naval Postgraduate School |
|
| Description |
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. Subjects: Automatic theorem proving; Information asymmetry |
|
| Language | English | |
| Publication date | June 2006 | |
| Current location |
IA Collections: navalpostgraduateschoollibrary; fedlink |
|
| Accession number |
annalysisofspecw109452764 |
|
| Source | ||
| Permission (Reusing this file) |
Approved for public release, distribution unlimited | |
Licensing
[edit]
|
This work is in the public domain in the United States because it is a work prepared by an officer or employee of the United States Government as part of that person’s official duties under the terms of Title 17, Chapter 1, Section 105 of the US Code.
Note: This only applies to original works of the Federal Government and not to the work of any individual U.S. state, territory, commonwealth, county, municipality, or any other subdivision. This template also does not apply to postage stamp designs published by the United States Postal Service since 1978. (See § 313.6(C)(1) of Compendium of U.S. Copyright Office Practices). It also does not apply to certain US coins; see The US Mint Terms of Use.
|
 |
| This file has been identified as being free of known restrictions under copyright law, including all related and neighboring rights. | ||
File history
Click on a date/time to view the file as it appeared at that time.
| Date/Time | Thumbnail | Dimensions | User | Comment | |
|---|---|---|---|---|---|
| current | 13:38, 14 July 2020 |  | 1,275 × 1,650, 112 pages (472 KB) | Fæ (talk | contribs) | FEDLINK - United States Federal Collection annalysisofspecw109452764 (User talk:Fæ/IA books#Fork8) (batch 1993-2020 #7508) |
You cannot overwrite this file.
File usage on Commons
The following page uses this file: