2012 | OriginalPaper | Buchkapitel
Extensible Specifications for Automatic Re-use of Specifications and Proofs
verfasst von : Daniel Matichuk, Toby Murray
Erschienen in: Software Engineering and Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
One way to reduce the cost of formally verifying a large program is to perform proofs over a specification of its behaviour, which its implementation refines. However, interesting programs must often satisfy multiple properties. Ideally, each property should be proved against the most abstract specification for which it holds. This simplifies reasoning and increases the property’s robustness against later tweaks to the program’s implementation. We introduce
extensible specifications
, a lightweight technique for constructing a specification that can be instantiated and reasoned about at multiple levels of abstraction. This avoids having to write and maintain a different specification for each property being proved whilst still allowing properties to be proved at the highest levels of abstraction. Importantly, properties proved of an extensible specification hold automatically for all instantiations of it, avoiding unnecessary proof duplication. We explain how we applied this idea in the context of verifying confidentiality enforcement for the seL4 microkernel, saving us significant proof and code duplication.