File:Security modeling and correctness proof using Specware and Isabelle (IA securitymodeling109453834).pdf
Original file (1,275 × 1,650 pixels, file size: 724 KB, MIME type: application/pdf, 147 pages)
Captions
Captions
Summary[edit]
Security modeling and correctness proof using Specware and Isabelle
(   ) |
|
|---|---|
| Author |
|
| Title |
Security modeling and correctness proof using Specware and Isabelle |
| Publisher |
Monterey, California. Naval Postgraduate School |
| Description |
Security modeling is the foundation to formal verification which is a core requirement for high assurance systems. This thesis explores how security models can be built in a simple and expressive manner using the Metaslang specification language in Specware. The models are subsequently translated, via the Specware to Isabelle Interface, to be proven for correctness in Isabelle which is a generic, interactive theorem proving environment. It is found that the translation between Specware and Isabelle is almost seamless and there is much potential in the use of Isabelle/HOL to discharge proof obligations that arise in developing Specware specifications, although the actual proving requires substantial knowledge and experience in logical calculus. Subjects: |
| Language | English |
| Publication date | December 2008 |
| Current location |
IA Collections: navalpostgraduateschoollibrary; fedlink |
| Accession number |
securitymodeling109453834 |
| Source | |
| Permission (Reusing this file) |
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. As such, it is in the public domain, and under the provisions of Title 17, United States Code, Section 105, is not copyrighted in the U.S. |
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:51, 24 July 2020 |  | 1,275 × 1,650, 147 pages (724 KB) | Fæ (talk | contribs) | FEDLINK - United States Federal Collection securitymodeling109453834 (User talk:Fæ/IA books#Fork8) (batch 1993-2020 #27246) |
You cannot overwrite this file.
File usage on Commons
The following page uses this file: