Computer Science Department, University Of Waikato
Computer Science Seminar Room, G1.15
Two new notions of refinement for mCharts are introduced and compared 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.