Going with the flow: parameterized verification using message flows
M. Talupur, и M. Tuttle. FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, стр. 1--8. Piscataway, NJ, USA, IEEE Press, (2008)
Аннотация
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.
%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
}