Rewriting Approximations For Properties Verification Over CCS Specifications

Roméo Courbis (1, 2)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems

This paper presents a way to verify CCS (without renaming) specifications using tree regular model checking. From a term rewriting system and a tree automaton representing the semantics of CCS and equations of a CCS specification to analyse, an over-approximation of the set of reachable terms is computed from an initial configuration. This set, in the framework of CCS, represents an over-approximation of all states (modulo bisimulation) and action sequences the CCS specification can reach. The approach described in this paper can be fully automated. It is illustrated with the Alternating Bit Protocol and with hardware components specifications.

Domaines: Théorie et langage formel [cs.FL]

Roméo Courbis. Rewriting Approximations For Properties Verification Over CCS Specifications. 2010. ⟨hal-00530351v2⟩