Paper Info
Title
On the Role of Formal Methods in Software Certification: An Experience Report
Abstract
This paper describes how formal methods were used to produce evidence in a certification, based on the Common Criteria, of a security-critical software system. The evidence included a top level specification (TLS) of the security-relevant software behavior, a formal statement of the required security properties, proofs that the specification satisfied the properties, and a demonstration that the source code, which had been annotated with preconditions and postconditions, was a refinement of the TLS. The paper also describes those aspects of our approach which were most effective and research that could significantly increase the effectiveness of formal methods in software certification.
Year
DOI
Venue
2009
10.1016/j.entcs.2009.09.001
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
top level specification,software certification,common criteria,required security property,security,formal statement,formal verification,security-critical software system,certification,formal method,software,formal methods,security-relevant software behavior,formal specification,source code,experience report,software systems,satisfiability
Software engineering,Computer science,Design by contract,Formal specification,Software system,Theoretical computer science,Refinement,Common Criteria,Formal methods,Certification,Database,Formal verification
Journal
Volume
Issue
ISSN
238
4
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
3
0.46
14
Authors
1
Name
Order
Citations
PageRank
Constance L. Heitmeyer1898151.71