Goldson, D., Reeve, G. & Reeves, S. (2002). μ-Chart-based specification and refinement. In C. George & H. Miao (Eds.), Proceedings of 4th International Conference on Formal Engineering Methods, ICFEM 2002 Shanghai, China, October 21–25, 2002. (pp. 323-334).
Permanent Research Commons link: http://hdl.handle.net/10289/1530
We introduce two new notions of refinement for μ-charts and compare them with the existing notion due to Scholz. The two notions are interesting and important because one gives rise (via a logic) to a calculus for constructing refinements and the other gives rise (via model checking) to a way of checking that refinements hold. Thus we bring together the two competing worlds of model checking and proof.