Planning Proofs of Correctness of CCS Systems

Centre for Intelligent Systems and their ApplicationsThe specification and verification of communicating systems has captured increasing interest in the last decades. CCS, a Calculus of Communicating Systems [Milner 89a], was especially designed to help this enterprise; it is widely used in both industry and academia. Most efforts to automate the use of CCS for verification have centered around the explicit construction of a bisimulation [Park 81]. This approach, however, presents severe limitations to deal with systems that contain infinite states (e.g. systems with evolving structure [Milner 89a] or that comprise a finite but arbitrary number of components (e.g. systems with inductive structure [Milner 89a]). There is an alternative approach to verification, based on equational reasoning, which does not exhibit such limitations. This formulation, however, introduces significant proof search control issues, and, hence, has remained far less explored. This thesis investigates the use of explicit proof plans [Bundy 88] for problems of automatic verification in the context of CCS. We have conducted the verification task using equational reasoning, and centred on infinite state systems, and parameterised systems. A parameterised system, e.g. a system with inductive structure, circumscribes a family of CCS systems, which have fixed struture and finitely many states.To reason about theses systems, we have adopted Robin Milner's approach [Milner 89a], which advocates the use of induction to exploit the structure and/or the behavior of a system during its verification. To automate this reasoning, wehave used proof plans for induction [Bundy 88]- built within CLAM [Bundy et al 90b], and extended it with special CCS proof plans. We have implemented a verification planner by adding these special proof plans to CLAM. The system handles the search control problems prompted by CCS verification satisfactorily, though it is not complete. Moreover, the system is capable of dealing with the verification of finite state systems, infinite state systems, and parameterised systems, hence, providing a uniform method to analyse CCS systems, regardless of their state space. Our results are encouraging: the verification planner has been successfully tested on a number of examples drawn from the litereature. We have planned proofs of conjectures that are outside the domain of existing verification methods. Furthernore; the verification planning is fully automated. Because of this, even though the verification plan has still got plenty of room for improvement, we can state that proof planning can handle the equational verication of CCS systems, and, therefore, advocate its use within this interesting field