Rewriting Approximations For Properties Verification Over CCS Specifications
Résumé
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]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...