Certifying Domain-Specific Policies

Michael R. Lowry, Thomas Pressburger, Grigore Rosu

DOI 10.1109/ase.2001.989793 dblp

Abstract

Proof-checking code for compliance to safety policies potentially enables a product-oriented approach to certain aspects of software certification. To date, previous research has focused on generic, low-level programming-language properties such as memory type safety. In this paper we consider proof-checking higher-level domain-specific properties for compliance to safety policies. The paper first describes a framework related to abstract interpretation in which compliance to a class of certification policies can be efficiently calculated. Membership equational logic is shown to provide a rich logic for carrying out such calculations, including partiality, for certification. The architecture for a domain-specific certifier is described, followed by an implemented case study. The case study considers consistency of abstract variable attributes in code that performs geometric calculations in Aerospace systems.

BibTeX

@inproceedings{Lowry-al:ASE01,
  author    = {Michael R. Lowry and
               Thomas Pressburger and
               Grigore Rosu},
  title     = {Certifying {Domain-Specific} Policies},
  booktitle = {ASE},
  pages     = {81--90},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Certifying Domain-Specific Policies

Abstract

Related papers