1. The FCTOOLS User Manual (Version 1.0)
- Author
-
Bouali, Amar, Ressouche, Annie, Roy, Valérie, De Simone, Robert, Concurrency, Synchronization and Real-time Programming (MEIJE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre de Mathématiques Appliquées (CMA), Mines Paris - PSL (École nationale supérieure des mines de Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), INRIA, and MINES ParisTech - École nationale supérieure des mines de Paris
- Subjects
ALGORITHMS ,[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] ,DATA STRUCTURES ,COMMON FORMAT {\SC FC2} ,AUTOMATA ,BDDS ,NETWORKS OF COMMUNICATING PROCESSES ,VERIFICATION TOOLS - Abstract
We describe a set of modular extensions to our Auto/Graph verification toolset for networks of communicating processes. These software additions operate from a common file exchange format for automata and networks, called {\sc fc2}. Tool functionalities comprise graphical depiction of objects, global model construction from hierarchical descriptions, various types of model reductions and of verification of simple modal properties by observers, counterexample production and visualisation. We illustrate typical verification sessions conducted on usual academic examples: dining philosophers, mutual exclusion algorithms and round-robin schedulers. Based on previous experience of drastic state explosion problems we aim here at efficiency in implementation. We use both explicit representation techniques and implicit techniques such as {\sc BDD}s, with functional overlap at places.
- Published
- 1996