Abstract:
AUTO is a system designed at manipulations inside the MEIJE process calculus. It builds finite automata from terms denoting networks of communicating machines, and then allows various verifications to be made, by reducing the automata from various observational viewpoints. AutoGraph is the graphical interface for this system, offering syntax-free representation of terms of the calculus. This system is also used to draw the various finite automata resulting from the verification phase, then allowing to immediately see some correctness properties. In this paper we present a sample case study, illustrating the use of AUTO and AutoGraph.