For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 1995/11/25
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.