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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
- Foster, Simon; Zeyda, Frank; Woodcock, Jim: Isabelle/UTP: a mechanised theory engineering framework (2015)
- Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Showing invariance compositionally for a process algebra for network protocols (2014)
- Bourke, Timothy; van Glabbeek, Rob; Höfner, Peter: A mechanized proof of loop freedom of the (untimed) AODV routing protocol (2014)
- Butterfield, Andrew: The logic of $U\cdot(TP)^2$ (2013)
- Cavalcanti, Ana; Mota, Alexandre; Woodcock, Jim: Simulink timed models for program verification (2013)
- Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
- Wei, Kun; Woodcock, Jim; Burns, Alan: Modelling temporal behaviour in complex systems with Timebands (2013)
- Wei, Kun; Woodcock, Jim; Cavalcanti, Ana: \itCircus Time with reactive designs (2013)