Abstract:

We present the MEIJE Verification Tool Set, including the tools ATG, Mauto and FcTools. The Verification Tool Set provides means for: drawing and editing automata and hierarchical networks of automata; building finite automata from those drawings, or from programs in CCS, Meije, Lotos, or Esterel; perform this building in a compositional way, together with various notions of semantic minimizations and abstractions; display graphically the results, and extract diagnostic information from elements of the reduced models. We comment on various exemples and case studies, and we discuss the size limits of the ToolSet.