Certifying Domain-Specific Policies

Certifying Domain-Specific Policies

Michael Lowry and Thomas Pressburger and Grigore Rosu

ASE'01, IEEE, pp 81-90. 2001

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.

PDF, Slides(PPT), AutoFilter, DOI, ASE'01, BIB