hal-00530351, version 2
Rewriting Approximations For Properties Verification Over CCS Specifications
(2010-06-11)
Abstract: 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.
- 1:
- Université de Franche-Comté : EA4269
- 2:
- INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Formal Languages and Automata Theory
- Available versions : v1 (2010-10-29) v2 (2011-03-11)
- hal-00530351, version 2
- http://hal.archives-ouvertes.fr/hal-00530351
- oai:hal.archives-ouvertes.fr:hal-00530351
- From:
- Submitted on: Thursday, 10 March 2011 16:59:21
- Updated on: Wednesday, 23 November 2011 00:12:04
Associated documents
Export