A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicationg Finite-State Machines
-
- HIGUCHI M.
- Faculty of Engineering Science, Osaka University
-
- Shirakawa Osamu
- Sumitomo Metal Industries, LTD.
-
- Seki Hiroyuki
- Faculty of Engineering Science, Osaka University
-
- Fujii Mamoru
- College of General Education, Osaka University
-
- Kasami Tadao
- Advanced Institute of Science and Technology
この論文をさがす
抄録
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.
収録刊行物
-
- IEICE Trans. Commun., B
-
IEICE Trans. Commun., B 76 (11), 1363-1372, 1993
一般社団法人電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1570572702511030784
-
- NII論文ID
- 110003216877
- 10000014647
-
- NII書誌ID
- AA10826261
-
- ISSN
- 09168516
-
- 本文言語コード
- en
-
- データソース種別
-
- CiNii Articles