The Use of Conditional Grammars for Specifying and Verifying Communication Protocols

Petr Matousek
Dept. of Computer Science and Informatics
University of Technology Brno
Bozetechova 2, 612 66 Brno
Czech republic
E-mail: matousp@dcse.fee.vutbr.cz

Keywords: protocol, formal method, conditional grammar, verification, communication

Abstract

1  Introduction

For successful building of such system based on communication protocols formal specification and further analysis of the specified protocol is required. The specification should unambiguously describe the system, show its main features and behavior and - on the other hand - reveal possible bottle-necks and flaws in design. Formal specification is a good base for system verification and simulation.

Mostly the formal specification and testing is applied only on a simple version of a protocol, because standard formal methods for protocol description (regular grammars, finite state machines, Petri nets) are not suitable for the specification of a full protocol, e.g. with protocol parameters, time constraints etc. By that simplification the protocols are examined only from structural points of view.

The paper presents a new formal framework for the protocol specification based on conditional grammars. It is a part of the author's PhD. project ``Formal description and verification of a class of high-level protocols with real-time constraints''.

The first part of this paper introduces the motivation and a part of background theory of the presented work. In next parts the proposed theory is presented and demonstrated on an example. The last part of the paper resumes benefit of the proposed approach in protocol verification and depicts future steps of the research.

2  Theoretical background

The grammar is formally characterized by a tuple

G = (N, T, P, S),

where N is a final set of nonterminals, T is a final set of terminals, P is a set of rules and S is the starting nonterminal (S Î V).

Considering communication protocols, the set T is composed of symbols sent by both communicating parties (i.e. commands). Both set of production rules and set of nonterminals are constructed according to expected communication sequences. For a class of high-level communication protocols we expect a half-duplex communication channel, and the protocol to be of type request/response, i.e. every command sent by one partner (called request) yields appropriate response (confirmation, data, etc.).

Mostly only single commands without any additional information are supposed. This can model a simple structure of the system using, for instance, a finite state machine or regular grammar. However, response depends not only on a request command but mostly on request command parameters that determine an appropriate answer of the system.

The proposed formalism is based on conditional grammars. Its design is descriptive and easy to read. It provides formalism to define parameters as a part of terminals. Every rule contains a condition - to make behavior deterministic according to protocol parameters. Consequently, only those productions are applied on a sentential form that satisfy a corresponding condition evaluated by protocol parameters.

A global context conditional grammar (GCC-grammar) of degree i is according to [] a triple

(G,FOR,PER),

where G=(N,T,P,S) is a context free grammar, FOR Í (NÈT), and PER Í (V ÈN)⁺ such that y Î PER implies |x| £ i.

A context free grammar is a quadruple G = (N,T,P,S), where N, V and S have the same meaning as written above and every production in P is of the form A ® x , where A Î N, x Î (N ÈT)^*.

A production as A ® x Î P can be applied to a word w only when

(i) no forbidding symbol from FOR occurs in w, or
(ii) A occurs in a permitting word from PER which is a subword of w.

A global context conditional grammar works with static conditions, i.e. the definition of GCC grammar contains both sets FOR and PER, and conditions depends only on a current sentential form. For real world protocols those conditions that depend not only on a current sentential form but also on protocol parameters and the state of internal memory of the system are required.

The principle of the internal control is not new. In their work [,pp. 98-100], the authors introduce a cooperating distributed grammar system with memories (mCD grammar system). The system is based on semi-conditional grammars. The productions depend on a left-side nonterminal and as well on permitting and forbidding context conditions and the state of a memory string. The memory is implemented as a queue or a stack containing both terminals and nonterminals. Then rewriting is regulated by existence of a certain symbol in the memory string.

In our approach we propose a different view on context conditions. Just as in GCC grammar or in mCD grammar we test existence of a substring u in a given set or a memory string. Unlike GCC grammar our ``set FOR'' is not static but it is dynamically ``updated''. In contrast to mCD grammar we allow searching a substring along the whole sentential form, not only at the beginning or at the end.

Conditions in our case are represented in form of dynamic memory string - a sentential form that is rewrited by special grammar. This sentential form contains parameters of the protocol. Instead of rewriting the first or the last symbol of the memory string (as proposed by mCD grammar systems) we allow rewriting of any symbol within the memory string. Productions of this grammar supports adding of a parameter, deleting or testing the existence of a parameter in the memory string.

• A memory grammar is a quadruple G_m = (N_m = {S_m, Symbol(x)},T_m = {x},P_m,S_m), where P_m is a final set of productions of three types:

  • [(r₁)] S_m ® S_m  Symbol(x) ... addition rule
  • [(r₂)] Symbol(x) ® e ... deletion rule
  • [(r₃)] Symbol(x) ® Symbol(x) ... existential rule

In our proposal a parameter of a protocol command is a value associated with a terminal representing protocol command - for instance add_user(x) represents command add_user and its parameter x. The value is a part of a given sentential form closed in braces (). In one derivation step the values can be assigned to nonterminals as attributes (cf. attribute grammars []). Besides, they are evaluated and assigned using productions of context conditions.

For the use of parameters we define a grammar with parameters (GP) as a quadruple

G1 = (N1,T1,P1,S1),

where N₁ is a final set of nonterminals, T₁ a final set of terminals, P₁ is a set of semantic productions, and S₁ is the starting symbol. Productions are of form

• (A ® x; Æ), where A Î N₁, x Î (N₁ ÈT₁)^*, or
• (A ® xy(a)z; C.par = a), where A Î N₁, x,z Î (N₁ÈT₁)^*, y(a) Î T₁×N₁ and C Î N₁ is a right side nonterminal of this production.

A production can contain a semantic part that assigns a value of parameter a to a nonterminal on the right site of a production. Values of parameters are stored in a similar way like attributes in the attribute grammar.

Roughly speaking, the GP grammar is a context free grammar with some internal semantic actions.

Let u,v Î (N₁ ÈT₁)^*. Then we say u directly derives v according to A ® y or A ® y(a), denoted by u Þ v   [p], if exists p Î P₁, p = A ® y or A ® y(a) and u = xAz, v = xyz or v = xy(a)z for some x,y,z Î (N₁ÈT₁)^*, y(a) Î T₁×N₁.

Now, we define a grammar system with conditions and parameters (GCP). A GCP grammar system is a tuple G = (G,G₁,S), where

1. [(i)] G₁ is GP grammar G₁ = (N₁,T₁,P₁,S₁) as defined above
2. [(ii)] G is a quadruple (N,T,P,S), where

   • N = {N₁ È{S} ÈN_m = {S_m, Symbol(a)}}
   • T = {T₁ È{a}}
   • P is a final set of production of form

     1. p = (A ® x; Æ; r), or
     2. p = (A ® xy(a)z; C.par = a; r)
     where C Î N is a substring of x, A Î N, x,z Î (NÈT)^*, y(a) Î (N ×T) and r is either one production from a set R

     • [(r₁)] {(S_m® S_m  Symbol(x)),
     • [(r₂)] (Symbol(x) ® e),
     • [(r₃)] (Symbol(x) ® Symbol(x))},
     or empty set Æ.
3. [(iii)] S is the starting symbol in a form (S₁; S_m)

Let u,v Î (N ÈT)^*, m,m¢ Î {S_m, Symbol(a)}^*, u = (xAz;m), v = (xyz;m¢) for some x,y,z Î (NÈT)^*. Then we say u directly derives v according to p = (A ® y; Æ,r) or p = (A ® y(a);C.par = a;r), denoted by u Þ v   [p], iff p Î P and one of the following conditions holds:

• (i) r is empty set Æ, or
• (ii) exists r Î R such that m Þ m¢[r].

In the standard manner, we can define Þⁱ (for i ³ 0), Þ^*, Þ⁺.

The language of G, denoted by L(G), is defined by

L(G) = {(w;m) Î (T*;m Î Nm*)  |  (S;Sm) Þ* (w;m)}.

Language L(G) describes a protocol sentence accepted by the protocol defined using grammar G. In comparison with other approaches the specification includes parameters of the protocol and the memory that represents the internal state of the protocol. This brings us advantages as follows:

• A protocol is specified using simple context free grammar which is easy to create and read.
• Protocol parameters are added to a grammar definition and to a sentential form in a descriptive form.
• Context conditions are defined in a form of productions over memory that contains parameters. A string of parameters (the memory) represents dynamic set of context conditions. Using special grammar we are not limited by certain number and type of parameters and before applying any rule we can test their existence in a memory string.
• Memory string evolves in the course of rewriting. At the end it represents a state of a system after protocol operation. This can be used for server/client simulation.