Protocol Verification Tool with Extended Petri Net and Horn Clause

Takashi WATANABE; Tsuyoshi OHTA; Fumiaki SATO; Tadanori MIZUNO

Protocol Verification Tool with Extended Petri Net and Horn Clause

Takashi WATANABE, Tsuyoshi OHTA, Fumiaki SATO, Tadanori MIZUNO

Full Text Views

0

Share
Cite this

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

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://globals.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 -