Proving refinement using transduction

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfællebedømt

Standard

Proving refinement using transduction. / Rump, Camilla Østerberg; Jonsson, Bengt; Pnueli, Amir.

I: Distributed Computing, 05.1999, s. 129-149.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfællebedømt

Harvard

Rump, CØ, Jonsson, B & Pnueli, A 1999, 'Proving refinement using transduction', Distributed Computing, s. 129-149.

APA

Rump, C. Ø., Jonsson, B., & Pnueli, A. (1999). Proving refinement using transduction. Distributed Computing, 129-149.

Vancouver

Rump CØ, Jonsson B, Pnueli A. Proving refinement using transduction. Distributed Computing. 1999 maj;129-149.

Author

Rump, Camilla Østerberg ; Jonsson, Bengt ; Pnueli, Amir. / Proving refinement using transduction. I: Distributed Computing. 1999 ; s. 129-149.

Bibtex

@article{c610759121ef4d8986f63c94ba9f1245,
title = "Proving refinement using transduction",
abstract = "When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary. An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.",
author = "Rump, {Camilla {\O}sterberg} and Bengt Jonsson and Amir Pnueli",
year = "1999",
month = may,
language = "English",
pages = "129--149",
journal = "Distributed Computing",
issn = "0178-2770",
publisher = "Springer",

}

RIS

TY - JOUR

T1 - Proving refinement using transduction

AU - Rump, Camilla Østerberg

AU - Jonsson, Bengt

AU - Pnueli, Amir

PY - 1999/5

Y1 - 1999/5

N2 - When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary. An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.

AB - When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary. An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.

M3 - Journal article

SP - 129

EP - 149

JO - Distributed Computing

JF - Distributed Computing

SN - 0178-2770

ER -

ID: 227094574