Sciweavers

AINA
2003
IEEE

Formal Verification of Condition Data Flow Diagrams for Assurance of Correct Network Protocols

14 years 1 months ago
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 a...
Shaoying Liu
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where AINA
Authors Shaoying Liu
Comments (0)