Anzeige
Erschienen in:
2017 | OriginalPaper | Buchkapitel
19. On Combining Algebraic Specifications with First-Order Logic via Athena
verfasst von : Katerina Ksystra, Nikos Triantafyllou, Petros Stefaneas
Erschienen in: Algebraic Modeling of Topological and Computational Structures and Applications
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
Abstract
We present a verification framework developed by researchers of the National Technical University of Athens as part of the Research Project Thalis “Algebraic Modeling of Topological and Computational Structures and Applications”. The proposed framework combines two different specification and theorem-proving systems, in order to facilitate the modeling and analysis of critical software systems. On the one hand, the CafeOBJ algebraic specification language offers executable, composable specifications, and insightful information about the proofs of desired invariant properties. On the other hand, Athena, an interactive theorem-proving system, provides automation and soundness guarantees for its results, as well as detailed structured proofs. Although having conducted complicated case studies (references to which are provided in the paper), here we focus on explaining the steps of the proposed hybrid methodology as clearly as possible, through an illustrative example of a simple mutual exclusion protocol.