Deriving Synchronisation Protocols in Circus
Jim Woodcock*
University of Kent
Circus combines Z, CSP, and the refinement calculus, and is being
used to support the verification of flight control software in
industry. The formal semantics of Circus are based on Hoare & He's
unifying theories of programming, and underpin a refinement
calculus for reasoning about reactive systems. We illustrate this
calculational approach by deriving synchronisation protocols that
are needed to implement the control laws for an unmanned autonomous
aircraft.
* Jim Woodcock is Professor of Software Engineering at the University of
Kent at Canterbury, where he works with the Systems Engineering
Research Group.
