Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Isabelle/Circus: A Process Specification and Verification Environment
verfasst von : Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff
Erschienen in: Verified Software: Theories, Tools, Experiments
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
The
Circus
specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He’s unifying theories of programming (UTP).
We develop a machine-checked, formal semantics based on a “shallow embedding” of
Circus
in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and implement tactic support that finally allows for proofs of refinement for
Circus
processes (involving both data and behavioral aspects).
This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of
Circus
.