Automated Verification of Safety Requirements using CCS and Binary Decision Diagrams

Abstract

There is a growing interest in the application of formed methods in the software development process, especially in the area of safety critical applications. Formal verification, however, often requires a high effort. With the availability of automated methods this effort could be largely reduced and thus enable a more widespread application of formal methods. Process Calculi like CCS are a common formalism for modelling and verification of protocols and distributed applications. A major problem in computer-aided verification of CCS models is the inevitable combinatorial state space explosion. Existing verification tools mostly operate on an explicit representation of the state space in form of a labelled transition system (LTS), and often already fail in establishing this LTS. Binary Decision Diagrams (BDDs) are based on a compact, implicit representation of transition systems and state sets and therefore offer a promising alternative. In this paper we describe the implementation of such a verification tool based on BDDs. The tool accepts CCS-definitions, automatically derives suitable encodings of states and actions and creates an efficient encoding of the LTS which accounts for the structure of the modularized CCS-hierarchy. Additionally it ensures that the specification models a finite transition system. The efficiency of this method will be investigated with two examples where the first is Milners well known scheduler, which is mostly of academic relevance as a benchmark for verification tools. The second example, which is of more practical interest, considers the popular CSMA/CD-communication protocol, including propagation delays on the communication channel. As such it allows more relevant conclusions about the appropriateness of the created tool.