Abstract. We present a practical approach to a formal analysis of UMLbased models. This is achieved by an underlying formal representation in Z, which allows us to pose and dischar...
Circus is a combination of Z, CSP, and Morgan’s refinement calculus; it has an associated refinement strategy that supports the development of reactive programs. In this work, ...