%0 Conference Paper %1 1517434 %A Talupur, Murali %A Tuttle, Mark R. %B FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design %C Piscataway, NJ, USA %D 2008 %I IEEE Press %K concurrency infinite_state invariant parameterized verification %P 1--8 %T Going with the flow: parameterized verification using message flows %U http://portal.acm.org/citation.cfm?id=1517434 %X 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 abstracting 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 with any sound abstraction procedure. This facilitates the use of a new abstraction 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. %@ 978-1-4244-2735-2

@inproceedings{1517434, abstract = {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 abstracting 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 with any sound abstraction procedure. This facilitates the use of a new abstraction 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.}, added-at = {2010-04-25T21:12:59.000+0200}, address = {Piscataway, NJ, USA}, author = {Talupur, Murali and Tuttle, Mark R.}, biburl = {https://www.bibsonomy.org/bibtex/2c480d1b45edafc0415cf00d2adb4f79e/giuliano.losa}, booktitle = {FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design}, description = {Going with the flow}, interhash = {2645f944eae3ee76c485e76b677e008f}, intrahash = {c480d1b45edafc0415cf00d2adb4f79e}, isbn = {978-1-4244-2735-2}, keywords = {concurrency infinite_state invariant parameterized verification}, location = {Portland, Oregon}, pages = {1--8}, publisher = {IEEE Press}, timestamp = {2010-04-25T21:12:59.000+0200}, title = {Going with the flow: parameterized verification using message flows}, url = {http://portal.acm.org/citation.cfm?id=1517434}, year = 2008 }