Protocol Verification Tool with Extended Petri Net and Horn Clause

Takashi WATANABE  Tsuyoshi OHTA  Fumiaki SATO  Tadanori MIZUNO  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E78-A   No.11   pp.1458-1467
Publication Date: 1995/11/25
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Net Theory and Its Applications to Discrete Event System Design)
communication networks and services,  protocol verification,  Petri net,  Prolog,  Horn clause,  

Full Text: PDF(765.1KB)
>>Buy this Article

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.