IEICE TRANSACTIONS on Fundamentals
Protocol Verification Tool with Extended Petri Net and Horn Clause
Summary :
This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E78-A No.11 pp.1458-1467
- Publication Date
- 1995/11/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Net Theory and Its Applications to Discrete Event System Design)
- 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
Takashi WATANABE, Tsuyoshi OHTA, Fumiaki SATO, Tadanori MIZUNO, "Protocol Verification Tool with Extended Petri Net and Horn Clause" in IEICE TRANSACTIONS on Fundamentals,
vol. E78-A, no. 11, pp. 1458-1467, November 1995, doi: .
Abstract: This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e78-a_11_1458/_p
Copy
@ARTICLE{e78-a_11_1458,
author={Takashi WATANABE, Tsuyoshi OHTA, Fumiaki SATO, Tadanori MIZUNO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Protocol Verification Tool with Extended Petri Net and Horn Clause},
year={1995},
volume={E78-A},
number={11},
pages={1458-1467},
abstract={This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - Protocol Verification Tool with Extended Petri Net and Horn Clause
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1458
EP - 1467
AU - Takashi WATANABE
AU - Tsuyoshi OHTA
AU - Fumiaki SATO
AU - Tadanori MIZUNO
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E78-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 1995
AB - This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.
ER -
English
