Planning Equational Verification in CCS

9 years 6 months ago
Planning Equational Verification in CCS
Most efforts to automate formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems and hence there is interest in a novel class of problems, which we call VIPS, involving value-passing, infinite-state, parameterised systems. Existing approaches using model checking over FSSs are insufficient for VIPSs, due to their inability both to reason with and about domain-specific theories, and to cope with systems having an unbounded or arbitrary state space. We use a Calculus of Communicating Systems (CCS) [13] with parameterised constants to express and specify VIPSs. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems, regardless of their state space, and the data such systems communicate. Automating theorem proving in this system is an extremely difficult task. We provide automated methods for CCS analysis; they are app...
Raul Monroy, Alan Bundy, Ian Green
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where KBSE
Authors Raul Monroy, Alan Bundy, Ian Green
Comments (0)