Formal verification of Condition Data Flow Diagrams for assurance of correct network protocols

Condition Data Flow Diagrams (CDFDs) are a formalized notation resulting from the integration of Yourdon Data Flow Diagrams, Petri Nets, and pre-post notation. They are used in the SOFL (Structured Object-Oriented Formal Language) specification language to describe the architecture of formal specifications for network protocols and general dependable systems by defining data flow communications among processes. A large-scale specification is usually modeled as a hierarchy of CDFDs resulting from decomposing processes at various levels into CDFDs. To ensure that a decomposed CDFD is correct with respect to its high level process, verification is essential. However, how to verify rigorously the correctness of CDFDs is still an open problem. In this paper we address this problem by establishing a logical system consisting of inference rules for reasoning about CDFDs, and putting forward both formal proof and specification simulation as potential methods for correctness verification. We also give algorithms for deriving pre and postconditions of CDFDs and examples of verifying their correctness.