Formal Modeling of Communication Protocols by Graph Transformation

Formal modeling is a crucial first step in the analysis of safety critical communication protocols such as IP Telephony. These protocols are notoriously resistant to formal modeling due to their sheer size and complexity. We propose using graph transformation, a straight forward, visual approach to do this. In experiments with Distributed Feature Composition (DFC) protocol and its implementation in BoxOs, we find that graph transformation offers several key advantages over naive methods in modeling the dynamic evolution of a reactive communication protocol. The generated model closely follows the way in which communication protocols are typically separated into three levels: the first describing local features or components, the second characterizing interactions among components, and the third showing the evolution of the component set. The graph transformation semantics described here follows this scheme, enabling a clean separation of concerns when describing a protocol. Using DFC s...

• Type: Conference
• Year: 2006
• Where: FM
• Authors: Zarrin Langari, Richard J. Trefler
• Keywords: Communication Protocols, FM 2006, Formal Methods, Formal Modeling, Graph Transformation