A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines
スポンサーリンク
概要
- 論文の詳細を見る
This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.
- 社団法人電子情報通信学会の論文
- 1993-11-25
著者
-
Kasami Tadao
Advanced Institute Of Science And Technology
-
Seki Hiroyuki
Faculty of Engineering Science, Osaka University
-
Shirakawa Osamu
Sumitomo Metal Industries Ltd.
-
Higuchi Masahiro
Faculty of Engineering Science, Osaka University
-
Fujii Mamoru
College of General Education, Osaka University
-
Fujii Mamoru
College Of General Education Osaka University
-
Higuchi Masahiro
Faculty Of Engineering Kansai University
-
Higuchi Masahiro
Faculty Of Engineering Science Osaka University
-
Seki Hiroyuki
Faculty Of Engineering Science Osaka University
関連論文
- A System for Deciding the Security of Cryptographic Protocols (Special Section on Cryptography and Information Security)
- A Translation Method from Natural Language Specifications of Communication Protocols into Algebraic Specifications Using Contextual Dependencies
- 2-P-42 Effect of low-intensity cycling exercise with skin cold stimulation on intramuscular oxygen saturation(The Proceedings of the 17th Annual Meetings of Japan Society of Exercise and Sports Physiology Jury 25-26, (Tokyo))
- A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines
- Preparation of Superconductive (Bi, Pb)-Sr-Ca-Cu-O Thick Films by Rapid Quenching
- A Distributed Scheduling Algorithm Using Serialization Graph Testing with Fractional Tag
- Optimization of Grinding Conditions with Genetic Algorithm
- Protein Synthesis Algorithm and a New Metaphor for Selecting Optimum Tools
- A Concurrency Control Algorithm Using Serialization Graph Testing with Write Deferring