In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. E78-A, No. 11, pages 1458-1467. 1995.
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. In all-in-one method all descriptions are translated into Prolog clause and simulated exhaustively, whereas in hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the 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 alternative bit protocol to discuss its effectiveness.
Keywords: Horn clauses, PROLOG, Petri nets, Protocol verification, alternating bit protocol, communication networks, communication services.