Using Circus for Safety-critical Applications

AbstractCircus 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