Paper Info
Title
Rewriting approximations for properties verification over CCS specifications
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.
Year
DOI
Venue
2011
10.1007/978-3-642-29320-7_20
FSEN
Keywords
Field
DocType
ccs specification,tree regular model checking,reachable term,alternating bit,initial configuration,properties verification,hardware components specification,tree automaton,modulo bisimulation
Programming language,Model checking,Computer science,Alternating bit protocol,Modulo,Theoretical computer science,Bisimulation,Rewriting,Tree automaton,Semantics
Conference
Citations 
PageRank 
References 
1
0.37
20
Authors
1
Name
Order
Citations
PageRank
Roméo Courbis1182.02