Verifying Trace Equivalence of a Shared-Memory-Style Communication System(<Special Section>Selected Papers from the 17th Workshop on Circuits and Systems in Karuizawa)
スポンサーリンク
概要
- 論文の詳細を見る
This paper describes a formal verification for a sharedmemory-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 [3], 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.
- 社団法人電子情報通信学会の論文
- 2005-04-01
著者
-
Kawabe Yoshinobu
Ntt Corp. Atsugi‐shi Jpn
-
Kawabe Yoshinobu
Ntt Communication Science Laboratories Ntt Corporation
-
Mano Ken
NTT Communication Science Labs.
-
Mano Ken
Ntt Communication Science Laboratories
-
Mano Ken
Ntt Corp. Atsugi‐shi Jpn
関連論文
- A new proof of Chew's theorem(Theory of Rewriting Systems and Its Applications)
- Termination of Order-Sorted Rewriting with Non-minimal Signatures
- Name Creation Implements Restriction in the π-Calculus
- On Backward-Style Anonymity Verification
- An Adversary Model for Simulation-Based Anonymity Proof
- A Metric Semantics for the $\pi$-Calculus Extended with External Events(Concurrency Theory and Applications '96)
- Verifying Trace Equivalence of a Shared-Memory-Style Communication System(Selected Papers from the 17th Workshop on Circuits and Systems in Karuizawa)
- Modularity of Confluence in Order-Sorted Term Rewriting Systems