Table of Contents

• Process Algebra
• Verification
• Fc2 format
• Autograph (Atg)
• Fc2Tools

Process Algebra

Process algebra theory is now well-established as a powerful mathematical model of concurrency, allowing for instance representation and further analysis of distributed systems and algorithms, protocols and many other topics inside and outside computer science.

Process algebra syntax allows for hierarchical description of systems, an invaluable feature later for compositional reasoning, verification and analysis. The few conceptual operators, on the other hand, allow immediately understandable graphical counterparts. autograph is a graphical editor specific to the representation of process algebraic terms, and the display of analysis information on them.
Process algebra semantics provides straightforward "structural" interpretation into labeled transition systems. When restricted to the finite state case (static networks of automata basically), reasoning can be fully automated, resulting in model-checking where the underlying model is confronted to modal properties. Such properties can be presented as logic formulae, or themselves as specification automata. Precise notions of property satisfaction must be defined then, mostly according to dual views of future in compurtation as as either branching-time or linear-time.

Verification

Most research in model-checking is concerned with complexity of dedicated algorithms, to cope with intrinsic state explosion in the global description of distributed systems with asynchronously evolving processes. The prevailing approaches are:

Compositional Reductions

This comprises: state quotient by identification of equivalent states, for equivalences such as (branching-time) bisimulation or (linear-time) trace-language equality; behaviour identification by hiding of local ones; behaviour constraint by representation of contexts. Such minimisation operations on labelled transition systems, and most of all their compositional application along syntactic lines, form the algorithmic core of Auto and its further extensions Fc2Tools.

Abstraction

Reversing usual top-down refinement approach, abstraction allows to extract from concrete casualties of systems, providing a simpler view on it. Auto comprises functions for behavioural abstraction whereby sequences of actions, considered as transactions, are replaced by a single named abstract behaviour.

Implicit State Representation

Use of binary decision diagrams have greatly enhanced the representation ability by allowing symbolic representation of state spaces (as a minimal shared graph represnting the characteristic function of reachable states inside a boolean variables encoding of the full problem). BDDs are specially efficient in some types of verification (typically in forward search and reachability analysis, possibly in presence of observers). In other cases explicit enumeration methods may still win in complexity, when applicable (typically for bisimulation minimisation). Our "next generation" Fc2Tools package divides in two: fc2implicit implements verification and analysis using BDDs, while fc2explicit uses classical enumeration style.
Other efficient means of state representation exist, using hashing techniques for capture of states with high probability.

On-the-Fly Model-Checking

There the property to be established is used to guide the search into the state space of the analysed process. This technique is most beneficial when the property takes the form of an observer, with notification terminal states, and verification is conducted as product of state machines. Then implicit representation methods prove efficient. If the specification represents some liveness property (on infinite sequences), fairness assumptions on the process may have to be added.
In the case of finite behaviours, abstraction can be seen as a generalisation of (single result) observers. Abstraction also notices (infinitary) loops in the process. In addition of abstraction, Fc2Tools implements on-the-fly comparison with a deterministic observer.

Fc2 format

By nature verification systems contains heterogeneous algorithmic functions and methods, resulting hopefully in a wealthy modular toolset. Connecting and combining elements of this toolset, and at a larger level of different existing verification systems, is an interesting challenge. It requests existence of interface file formats. We proposed such a format for representation of reactive automata and network transducers named Fc2, and used it to connect our "next-generation" of modular tool elements. Reference manual and a yacc grammar of the representation format are available by ftp.

Autograph (Atg)

Autograph (also named atg) is a graphical editor for process algebra terms and automata, hopefully as simple and powerful as you need it to be.
Representation is natural and immediate, as seen on the following image.

Autograph pictures are translated into Fc2 format for interface with verification modules. Conversely, autograph reads Fc2 description of automata (and not yet networks, sorry), letting users progressively unfold their lay-out.
Editing functions in autograph contains some placement facilities, while this aspect was not our major design concern.

Fc2Tools

As already mentioned, verification modules are often implemented in a redundant fashion using both explicit and implicit representation of global states.
As a rule of thumb fc2implicit favors a style of verification based on observers, and generally on forward search of the reachable state space under "guidance" of a property to check. Safety properties with a linear-time view of systems are easily captured that way.
On the other hand, fc2explicit favors compositional reduction of systems with a strong abstraction on actual behaviours (hiding), and with a branching-time view of systems (bisimulation).