Keywords: protocol, formal method, conditional grammar, verification, communication
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.
The grammar is formally characterized by a tuple
|
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
|
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
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.
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
|
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 Î (N1 ÈT1)*. Then we say u directly derives v according to A ® y or A ® y(a), denoted by u Þ v [p], if exists p Î P1, p = A ® y or A ® y(a) and u = xAz, v = xyz or v = xy(a)z for some x,y,z Î (N1ÈT1)*, y(a) Î T1×N1.
Now, we define a grammar system with conditions and parameters (GCP). A GCP grammar system is a tuple G = (G,G1,S), where
Let u,v Î (N ÈT)*, m,m¢ Î {Sm, 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:
In the standard manner, we can define Þi (for i ³ 0), Þ*, Þ+.
The language of G, denoted by L(G), is defined by
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:
Request commands ADD_USER, REMOVE_USER contain a parameter - username. According to the value of the parameter corresponding answer is generated.
For instance, possible answers for command ADD_USER are USER_ADDED or ALREADY_EXISTS. Regular grammar would apply one of these answers in a non-deterministic way. But the answer depends good deal on an argument (parameter) of the command. Considering e.g. argument username we can determine the answer after evaluation of that argument.
Context free grammar G=(N,T,P,S) of the system is defined as follows:
Now we add parameters (semantic action) to this grammar so a new GP grammar is G1 = (N1 = {NÈ{a}},T,P1,S1). Set of productions P1 is following:
A GCP system of this system is a triple G = (G,G2,S), where
Here, there are some examples of derivation process:
This paper introduces a new uniform technique for formal specification of high-level communication protocols. It is based on conditional grammars theory. The paper shows a complete theory and demonstrates the proposed approach on a simple example. Because of its descriptive power seems to be a good tool for real-world protocol specification.
Using GCP grammar we can describe a communication protocol more precisely - parameters are part of the language. In addition context conditions specify how communication partners behave depending on parameters - that is very useful for implementation. Because of the formal description we can use various verification techniques to prove that the communication system responses as expected. Future work is focused on protocol verification using PVS (Prototype Verification System) and definition of real-time constraints as a part of the GCP language.
L(G) = {(w;m) Î (T*;m Î Nm*) | (S;Sm) Þ* (w;m)}.
3 Case study
The formalism introduced in the previous part is demonstrated on a simple communication protocol of user database. Following requests are implemented: ADD_USER, REMOVE_USER, BYE, and corresponding answers: USER_ADDED, USER_REMOVED, ALREADY_EXISTS, NO_SUCH_USER.
(A ® remove_user(a) C; C.par = a),
(A ® bye;Æ),
(B ® already_exists A;Æ),
(C ® no_such_user A ; Æ)}
(A ® remove_user(a) C;
C.par = a;Æ),
(A ® bye;Æ;Æ),
Sm ® User(B.par) Sm),
(B ® already_exists A;Æ;
User(B.par) ® User(B.par)),
User(C.par) ® e),
(C ® no_such_user A ; Æ;Æ)}
4 Conclusion
Acknowledgment
The work presented here in the paper is a part of a project supported by grant FRVS no. 99/2001 ``Selection of methods for formal specification and verification of communication protocols'' of Czech Ministry for Education. The author is indebted to Dr. Alexander Meduna and Martin Svec for their valuable suggestions and advises about the grammar systems.
References
Biography
Petr Matousek was born in Ústí nad Labem, Czech republic and went to University of Technology Brno, where he received in 1997 an MSc. degree in Informatics and Computer Science. In 1997-1998 he worked at CERN, Geneva in IT division on the project of global distributed LDAP directory. Since 1998 he continues his PhD. studies at University of Technology, Brno, focused on formal description and verification of protocols with real-time constraints. He externally teaches at the University.
Contact - http://www.fee.vutbr.cz/~matousp.