1 Background

  Using formal methods to specify systems becomes more and more a necessity to get round the increasing system complexity. In this paper, we present the use of formal methods throughout system specifications. More precisely, our work is based on TMN (Telecommunication Management Network), so the subject matter being the use of formal methods to specify distributed systems.

Distributed systems are often represented as a set of objects distributed on networks. An object is composed of some data and offers some services. An object specification is an abstraction of object data and services which is independent of its implementation. Recently, the distributed systems development is based on the client/server paradigm. The client/server paradigm represents communication between two processes, the client and the server, the client requiring some services given by the server. In this paradigm, distributed systems are specified in terms of interfaces between objects. Some current specification languages (CORBA/IDL [COR93], DCE/IDL [KTW93], ODL [ODL96], etc) base their system representations on this paradigm. The IDL (Interface Definition Language) generic name is associated to these languages.

However, specifying object interfaces is not sufficient because IDL languages do not specify the system behaviour, or even the object behaviour. Object behaviours are related to object states. An object state is the set of data values and offered services that the object can deliver at a certain time. In fact, an object life is a sequence of states. In object state terms, an object behaviour can represent :

• an object invariant,
• an object state change,
• output values of object services.

An object invariant is a set of properties that are respected by all object states. For example, the number of subscribers that are referenced by a telephone dispatcher cannot exceed the dispatcher capacity.

An object state change is a set of properties that must be respected when an object switches state. A state change can be a consequence of :

• an object service out going call,
• an object service in coming call,
• a climatic event, or other non-formal events,
• etc

For example, the addition of a subscriber on a telephone dispatcher is an object state change behaviour.

An object services can have parameters, and particularly output parameters. During a service call, their output parameters take new values, so an object behaviour can specify these output values.

In the telecommunications world, object behaviours are defined by some specification languages (GDMO [GDM92], SNMP/MIB [RM90], etc), however, in these languages, behaviours are described informally. Our work is to simulate system specifications, so formalizing objects behaviour is of interest to us.

Object behaviour specification can be formulated using logical formalisms. An object state can be described by a formula if the formula is made true when the logical constants of the formula are mapped in the state computer variables, and we say that a state satisfies a formula if that formula describes it [Mor90]. In this context, an object invariant is the common logical assertion that the different states of the object satisfy, and an object service behaviour is a pair of pre and post-conditions (logical assertions). A pre-condition describes the object state before a service call, a post-condition describes the object state and the output values after a service call. An interpretation of a pair of pre/post-condition is : if the previous object state satisfies the pre-condition then the next object state satisfies the post-condition, otherwise we do not know what will happen.

To illustrate the use of logic to formalize object behaviours, we give the example of a telephone dispatcher object invariant and the pre and post-conditions description of its state change when the addition of a subscriber is realized :

• $n \leq l$
• [ n < l , n' = n + 1 ]

where n represents the number of subscribers that are constantly referenced by the telephone dispatcher, l is the capacity of the dispatcher, n and l are computer variables, but in logic, n and l are logical constants. In pre and post-condition description, an occurrence of n is decorated. This occurrence represents the value of n after the change of object state, the undecorated occurrences of n represent the value of n before the change of object state. Finally, only decorated variables are changed by a service call.

The use of logical assertions to specify object behaviours is compatible with existing distributed system specification languages. Many specification languages are defined on the object paradigm. Object oriented descriptions permit reuse, transparency, etc. For example,the inheritance concept maps reuse in object oriented descriptions. The above mentioned languages (CORBA/IDL, GDMO, ODL, etc) all respect inheritance of specialization [Boo92], i.e. a daughter interface is completely compatible with its mother interfaces. Figure 1 represents inheritance of object behaviour specified with logical assertions (in this figure, the $\Rightarrow$ symbol represents logical implication).

  

Figure 1: Inheritance of specialization a) of object invariants b) of pre/post-conditions

When a daughter interface inherits from a mother interface, the daughter interface behaviour is a composition of the mother interface behaviour, so the composition mechanism of logical assertions must respect the inheritance of specialization. For this, the composition mechanism proposed by EIFFEL [Mey92] respects the inheritance of specialization, and is reviewed in these expressions :

• $Inv2 = Inv1 \land AddInv$, by definition of conjunction, Inv2 is greater or equal to Inv1,
• $Pre2 = Pre1 \lor AddPre$, by definition of disjunction, Pre2 is smaller great or equal to Pre1,
• $Post2 = Post1 \land AddPost$, by definition of conjunction, Post2 is greater or equal to Post1.