TY - JOUR
T1 - Planning Proofs of Equations in CCS
AU - Monroy,R.
AU - Bundy,Alan
AU - Green,I.
PY - 2000/7
Y1 - 2000/7
N2 - 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, including a novel class of problems, which we call VIPS. VIPSs are value-passing, infinite-state, parameterised systems. Existing approaches using model checking over FSSs are insufficient for VIPSs. This is 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 the Calculus of Communicating Systems (CCS) (Communication and Concurrency. London: Prentice Hall, 1989) to express and specify VIPSs. We take program verification to be proving the program and its intended specification equivalent. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems and the data such systems communicate. Automating theorem proving in this context is an extremely difficult task.
We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the CL A M proof planner (Lecture Notes in Artificial Intelligence, Vol. 449, Springer, 1990, pp. 647, 648), we have implemented an automated verification planner capable of dealing with problems that previously required human interaction. This paper describes these methods, gives an account as to why they work, and provides a short summary of experimental results.
AB - 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, including a novel class of problems, which we call VIPS. VIPSs are value-passing, infinite-state, parameterised systems. Existing approaches using model checking over FSSs are insufficient for VIPSs. This is 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 the Calculus of Communicating Systems (CCS) (Communication and Concurrency. London: Prentice Hall, 1989) to express and specify VIPSs. We take program verification to be proving the program and its intended specification equivalent. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems and the data such systems communicate. Automating theorem proving in this context is an extremely difficult task.
We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the CL A M proof planner (Lecture Notes in Artificial Intelligence, Vol. 449, Springer, 1990, pp. 647, 648), we have implemented an automated verification planner capable of dealing with problems that previously required human interaction. This paper describes these methods, gives an account as to why they work, and provides a short summary of experimental results.
KW - CCS
KW - formal methods
KW - program verification
KW - automated reasoning
KW - Theorem proving
U2 - 10.1023/A:1008770222354
DO - 10.1023/A:1008770222354
M3 - Article
VL - 7
SP - 263
EP - 304
JO - Automated Software Engineering
T2 - Automated Software Engineering
JF - Automated Software Engineering
SN - 0928-8910
IS - 3
ER -