Verifying Trace Equivalence of a Shared-Memory-Style Communication System
Summary :
This paper describes a formal verification for a shared-memory-style communication system. We first describe two versions (i.e. abstract and concrete) of the communication system based on an I/O-automaton, which is a formal system for distributed algorithms. Then, we prove the concrete version can perform all the external operations of the abstract version. This result, together with a former result, leads to the equivalence of the two versions. The proof is done by Larch theorem prover, and is the ever largest case study using I/O-automata.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E88-A No.4 pp.915-922
- Publication Date
- 2005/04/01
- Publicized
- Online ISSN
- DOI
- 10.1093/ietfec/e88-a.4.915
- Type of Manuscript
- Special Section PAPER (Special Section on Selected Papers from the 17th Workshop on Circuits and Systems in Karuizawa)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Yoshinobu KAWABE, Ken MANO, "Verifying Trace Equivalence of a Shared-Memory-Style Communication System" in IEICE TRANSACTIONS on Fundamentals,
vol. E88-A, no. 4, pp. 915-922, April 2005, doi: 10.1093/ietfec/e88-a.4.915.
Abstract: This paper describes a formal verification for a shared-memory-style communication system. We first describe two versions (i.e. abstract and concrete) of the communication system based on an I/O-automaton, which is a formal system for distributed algorithms. Then, we prove the concrete version can perform all the external operations of the abstract version. This result, together with a former result, leads to the equivalence of the two versions. The proof is done by Larch theorem prover, and is the ever largest case study using I/O-automata.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e88-a.4.915/_p
Copy
@ARTICLE{e88-a_4_915,
author={Yoshinobu KAWABE, Ken MANO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Verifying Trace Equivalence of a Shared-Memory-Style Communication System},
year={2005},
volume={E88-A},
number={4},
pages={915-922},
abstract={This paper describes a formal verification for a shared-memory-style communication system. We first describe two versions (i.e. abstract and concrete) of the communication system based on an I/O-automaton, which is a formal system for distributed algorithms. Then, we prove the concrete version can perform all the external operations of the abstract version. This result, together with a former result, leads to the equivalence of the two versions. The proof is done by Larch theorem prover, and is the ever largest case study using I/O-automata.},
keywords={},
doi={10.1093/ietfec/e88-a.4.915},
ISSN={},
month={April},}
Copy
TY - JOUR
TI - Verifying Trace Equivalence of a Shared-Memory-Style Communication System
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 915
EP - 922
AU - Yoshinobu KAWABE
AU - Ken MANO
PY - 2005
DO - 10.1093/ietfec/e88-a.4.915
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E88-A
IS - 4
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - April 2005
AB - This paper describes a formal verification for a shared-memory-style communication system. We first describe two versions (i.e. abstract and concrete) of the communication system based on an I/O-automaton, which is a formal system for distributed algorithms. Then, we prove the concrete version can perform all the external operations of the abstract version. This result, together with a former result, leads to the equivalence of the two versions. The proof is done by Larch theorem prover, and is the ever largest case study using I/O-automata.
ER -
English
