Going with the Flow: Parameterized Verification Using Message Flows

A message flow is a sequence of messages sent among processors during the execution of a protocol, usually illustrated with something like a message sequence chart. Protocol designers use message flows to describe and reason about their protocols. We show how to derive high-quality invariants from message flows and use these invariants to accelerate a state-of-the-art method for parameterized protocol verification called the CMP method. The CMP method works by iteratively strengthening and ing a protocol. The labor-intensive portion of the method is finding the protocol invariants needed for each iteration. We provide a new analysis of the CMP method proving it works sound abstraction procedure. This facilitates the use of straction procedure tailored to our protocol invariants in the CMP method. Our experience is that message-flow derived invariants get to the heart of protocol correctness in the sense that only couple of additional invariants are needed for the CMP method to converge...

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Murali Talupur, Mark R. Tuttle
• Keywords: CMP Method, FMCAD 2008, Formal Methods, Message Flows, Protocol Invariants