160 / 1971-01-01 00:00:00

The Research And Model Checking Of Fairness Property In Concurrent System

Fairness constraints; PAT; Concurrent system; Linear Temporal Logic

In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system.We describe a formal methods to specify and check the Needham Schroeder Protocol(NS Protocol) under various fairness constraints. The NSP aims to establish mutual authentication between an initiator A and a responder B, after which some session involving the exchange of messages between A and B can take place. It is based on public key cryptography.We use the Linear Temporal Logic(LTL) for formalization and a Process Analysis Toolkit(PAT) for specification. We verified two properties of the NS Protocol, as a result, one property is valid, and other is not, for the invalid one, we get the counterexample.