Certifying domain-specific policies

Michael Lowry, Thomas Pressburger, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages81-90
Number of pages10
ISBN (Electronic)076951426X, 9780769514260
DOIs
StatePublished - 2001
Externally publishedYes
Event16th Annual IEEE International Conference on Automated Software Engineering, ASE 2001 - San Diego, United States
Duration: Nov 26 2001Nov 29 2001

Publication series

NameProceedings - 16th Annual International Conference on Automated Software Engineering, ASE 2001

Conference

Conference16th Annual IEEE International Conference on Automated Software Engineering, ASE 2001
Country/TerritoryUnited States
CitySan Diego
Period11/26/0111/29/01

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software
  • Safety, Risk, Reliability and Quality
  • Control and Optimization

Fingerprint

Dive into the research topics of 'Certifying domain-specific policies'. Together they form a unique fingerprint.

Cite this