Using Circus for Safety-critical Applications
Jim Woodcock · Electronic Notes in Theoretical Computer Science · 2004
Circus is language that unifies Z, CSP, and the refinement calculus, and we describe its application in the development of safety-critical systems. We show the descriptive power of Circus with a fragment of the formalisation of the steam boiler problem. We then use Circus's refinement calculus to bridge a semantic gap in development, where we eliminate a kind of abstract event.