communication protocol, formal specification, verification, PVS, theorem proving
For successful design and building of a real-world protocol formal specification of communication is required. The specification describes the system, shows its main features and behaviour and makes further analysis of the service possible. Formal specification is a good base for system verification and simulation that can reveal possible bottle necks and flaws in design.
This paper shows how Prototype Verification System (PVS) can be used for verification of high-level protocols. PVS [] is a verification system for writing formal specifications and checking formal proofs. It provides an integrated environment for the development and analysis of formal specifications, and supports a wide range of activities involved in creating, analyzing, modifying, managing and documenting theories and proofs.
The paper presents an example of the protocol verification on a simple protocol for user database access. The first part of the paper discusses a choise of formal methods for protocol description. The example is described using a regular grammar. Then it is shown how this regular grammar is represented by PVS description language. The second part of the paper deals with verification by PVS. It shows how some protocol properties can be specified using PVS language and verified by the prover. The last part of the paper summarizes current results and proposed future steps.
These tools and methods are not necessarily suitable for a class of high-level communication protocols. This class has some specific properties:
Most of the above mentioned methods are not applicable to a full-version protocol with parameters, time constraints, synchronization in distributed environment etc. For formal specification and verification a specification of a protocol is reduced. However, using that simplification the protocol is examined only from structural point of view. One possible solution to this problem is to use a more powerful specification system in contrast to, for instance, regular grammars. In [], there is proposed a new approach based on conditional grammars.
For our study, we can abstract out from a full-version protocols. Firstly, a simple version of a protocol is supposed. For formal description, regular grammar can be used.
The grammar is formally characterized by a tuple
|
Rewriting rules P of the grammar can be written as follows:
| S ® hello A A ® add_user B | remove_user C | bye B ® user_added A | invalid_user A | already_exists A C ® user_removed A | no_such_user A |
A language L = L(G) is a language of communication sequences of the system. Valid sentences of the language express possible communication sequences between a client and a server.
For verification of the system PVS theorem prover can be exploited. At first, the system specification has to be expressed as a theory in PVS language. Then, properties of the system are to be written as formulas in PVS language. Using theorem prover and tools integrated in PVS it can be proved if specified property holds or not. A successfully proved theory is displayed in LATEX format.
PVS theorem prover is based on Gentzen's formal axiomatic system, see further in []. Basic idea behind theorem proving is to describe a system by high-level functional description and specify desirable properties as theorems to be proved. These theorems are called putative theorems.
The point is that the process of proving putative theorems quickly highlights the gaps, errors, and inadequacies in the functional description. In some cases, such a proof could also prove that the system as described meets its complete specification, in other words, that it is correct. But it is rare that the proof succeeds. The typical proof attempt fails, but such failure usually yields valuable insights that can be used to correct oversights in the specification or formulation of the putative theorems.
The PVS proof checker is intended to serve as a skeptical party in a proving dialogue. The user supplies the steps in the argument and PVS applies them to the goal of the proof progressively breaking them into simpler subgoals or to obvious truths or falsehoods. If all the subgoals are reduced to obvious truths, the proof attempt has succeeded.
Several aspects of the language are built into the proof checker:
The most direct consequence of this is that the trivial, obvious, or tedious parts of the proof are often entirely hidden from the displayed proof.
| state: TYPE = {A, B, C, S, E} % states
input: TYPE = {hello,remove_user, add_user, bye, user_removed, no_such_user, user_added, already_exists}
automaton(st:state, inp: input): state = COND |
The specification of the protocol and auxiliary functions are written in PVS language. Then, it can be verified if an input sequence of commands belongs to language L(G), i.e. if it is a valid sentence of the protocol. In PVS a sequence of protocol commands becomes a theorem to be proved. If the proof is successful (the result is TRUE) the sequence is a valid protocol sentence according to the protocol specification. We implemented sequences of commands as lists of protocol requests and responses - see following example:
| % two valid protocol sequences
adduser: THEOREM IsValidSentence?((: hello, add_user, user_added, bye :)) % two invalid protocol sequences
short : THEOREM IsValidSentence?((: hello, bye, hello, add_user :)) |
In next step, the implementation of the protocol was extended by adding protocol parameters. The goal of our effort is to use PVS system for protocol verification AND simulation. That means not only test if an input sequence is a valid protocol sentence but also simulate behaviour of the protocol communication from a view of one dialogue partner. For example, we want to simulate what is the answer of the server to a specific request (sequence of commands) of the client.
| state: TYPE = {A, B1, B2, C1, C2, S, E, Error} % states
command: TYPE = {hello,remove_user,add_user,bye, user_removed,no_such_user,user_added, already_exists} % requests and responses
State: TYPE = [# st: state, db: userdb #] % State - record type
automaton(cstate:State, inp: command, args: t): State = |
Now, the protocol specification becomes more complicated - see Figure 3. States B and C are split into two new states B1, B2 and C1,C2. New states and transitions are added and the non-deterministic FSM is tranformed to a deterministic FSM. Transition from A to B1 depends not only on an input string but also on a condition which is specified as a predicate IsIndb?. If the predicate is true state B1 is reached. Otherwise, state B2 is reached. The new FSM is depicted on Figure .
Communication sequences of the system with parameters are specified in form of theorems as follows. An input is a pair of a command and a parameter. In the following example symbol e means empty parameter.
| % two valid protocol sequences adduser: THEOREM LET db:userdb = null IN CheckSentence((db,(: (hello,e), (add_user,a), (user_added,e), (add_user,a), (already_exists,e), (bye,e) :), null)) deluser: THEOREM LET db:userdb = null IN CheckSentence((db,(: (hello,e), (add_user,a), (user_added,e), (remove_user,a), (user_removed,e), (bye,e) :), null))
% two invalid protocol sequences |
Process of proving of the properties is still in progress. We try to prove theorems that contain higher order logic (quantifiers, for instance) and temporal logic. We want to find a strategy for protocol proving using PVS. Our goal is to show how PVS system can be exploited for protocol proving and what type of properties, proving strategies can be succesffully used. This paper demonstrates partial results of our research.
The paper shows an example of a simple protocol and its description by PVS language. Some properties of the protocol are specified as theorems in PVS language. Using PVS system their validity has been proved.
Future steps go further in protocol specification. High order logic and temporal logic are used to specify general and temporal propeties of the protocol. Their proving is not simple. Our goal is to show how PVS system can be exploited for protocol proving, and to propose some strategies for protocol proving and specification of the properties.