Abstract
The Auto/Graph toolset developed in our group was a pioneering software for analysis and verification of networks of communicating processes. We describe here the next-generation Auto/Graph, consisting of a modular tool suite interfaced around a common file description format named Fc2. The format allows representation of single reactive automata as well as combining networks. This format was developed in the scope of Esprit BRA project 7166:Concur2.
In the new implementation, most analysis functions are implemented with redundancy using both explicit classical representation of automata, and also implicit state space symbolic representation using Binary Decision Diagrams. The two alternative techniques offer drastically different performances in different cases, and having both at hand in a unified framework is a valuable thing.
Both Fc2Explicit and Fc2Implicit commands perform synchronised product and reachable state space search. They can minimize results w.r.t. strong, weak, branching bisimulation notions, and produce the result as an Fc2 automaton. They can also abstract the system with a notion of “abstract actions”, each synthesizing a set of sequences of concrete behaviours (in this sense behavioural abstraction can be seen as reverse from refinement). In addition Fc2Implicit has a fast checker for deadlocks, live-lock or divergent states, for which it produces counterexample paths in case of existence, while Fc2Explicit allows compositional reduction techniques, mostly in case of “observational” bisimulation minimisations. Several extensions are still underway.
The tool suite is completed by the graphical editor Autograph, which allows for graphical depiction of automata and networks as well as recollection of some form of results.
The toolset is available by anonymous ftp. Information can be obtained from the WWW page http://cma.cma.fr/Verification/verif-eng.html, or by e-mailing to fc2team@cma.cma.fr.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouali, A., Ressouche, A., Roy, V., de Simone, R. (1996). The Fc2Tools set (tool demonstration). In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_57
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_57
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive