Department Of Computer Science, University of Waikato
Computer Science Seminar Room, G1.15
mCharts (MicroCharts) is a specification language for reactive systems. Specifications are based on finite state automata with the addition of hierarchical and compositional structuring mechanisms. A notion of refinement exists for mCharts along with rules for calculating possible refinements. Although these rules are sound, i.e. any refinement constructed by the rules is a valid refinement, they are not complete, i.e. given two arbitrary mCharts specifications it is not, in general, possible to show whether or not one is a refinement of the other. This seminar will present work on constructing a complete calculus for the refinement of mCharts.