Isabelle/Circus: A Process Specification and Verification Environment

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.