FACT: a Tool for Code Generation from Communicating Automata
Cinzia Bernardeschi, Gianluca Dini, Andrea Domenici · CINECA IRIS Institutial research information system (University of Pisa) · 2005
FACT (Finite Automaton Compilation Tool) is a tool for the generation of skeletal Java code from a graphical specification of a concurrent system given in terms of networks of communicating automata. The code implements the dynamic behavior of the set of concurrent automata, abstracting from data computation, and satisfies the constraints imposed by the specification. Moreover, global properties of the concurrent behavior of the system that are proved at the specification level are preserved by the implementation.