Subsections

• 2.1.1 An example of composition formalism
• 2.1.2 Introducing Time
• 2.1.3 Valuating Time

2.1 Composition schemas

 To deal with composition, we first need to understand how to describe components' behaviours, and then investigate how the different formalisms may be composed to describe the behaviour of the full system. For instance, [BS97] insists that not only should components specify what they do but also the minimal contracts their required components must obey.

Behaviours can be specified in at least two main ways : automaton or theory (logic). Properties can be specified through logic, whether modal or not, or in a form of an automaton.

In this position paper we will only cite a small subset of those ways.

2.1.1 An example of composition formalism

 

A guarded automaton is a way for describing the behavior of a component's internal state and set of operations acting on the component's state. Transitions describe how component's internal state changes through activation of the component's permitted operations.

More precisely, a guarded automaton is a finite state automaton whose states and edges are labeled by respectively an automaton state invariant and a tuple (o,g,a), where o is the name of an operation, g a guard (a predicate on the component internal state), and a an action (a change in the component's internal state). The intended semantics is as follow: an (automaton) state $\sigma$ refers to a set of component's internal valuations. The (automaton) state's invariant has to be true in all component states refered by this (automaton) state. Being in the (automaton) state $\sigma$, a transition to $\tau$ can be fired if there is an edge from $\sigma$ to $\tau$ labeled (o,g,a) such that the next to be done operation is o and the guard g evaluates to true. If the transition is fired, the action a changes the (model) states. The (automaton) state invariant in $\tau$ must then be verified by the new (model) state. For instance, consider a (circular) bounded buffer whose operations are get and put. It can be modeled as a three states automaton whose states are full (intended meaning : no element can be inserted), empty (intended meaning : no element can be retrieved) and partial (intended meaning : elements can be inserted and retrieved). Two indices, in and out respectively point to the element's insertion and retrieve buffer's location. Figure 2, on the left, shows the corresponding guarded automaton.

  

Figure 2: Guarded Automata of a circular bounded buffer (see 2.1.1).

Suppose we want to create a component that extends the previous bounded buffer with a get_rear operation (an operation retrieving the last insterted element). The guarded automaton at the right of figure 2 presents such an operation. The behavior of the extended bounded buffer can be described as a (guarded automaton) product where guards and invariants are ANDed.

But a more complicated example, where automata states are distincts, will require a more complicated set of composition rules. It may also appear that, for some properties, ORing, rather that ANDing, guards and invariants will be more appropriate.

2.1.2 Introducing Time

Two kinds of properties are of particular interest in the verification of systems, namely, safety and liveness. Temporal Logic [Eme90] helps in defining and verifiying properties on the sequence of timed events, that is their relative order in time of their occurrence. Composition reasonning shemas like compositional minimization and assume/guarentee have been investiguated [CLM89,GL94] but seem not to have received enough attention to be at the point of being transferrable into industry. Moreover, timing constraints being our main topic rather the pure partial order of events, we turned to the timed automata extensions we will speak about now.

2.1.3 Valuating Time

Precise timing valuation are needed in critical systems. Modelisation decisions like linear versus branching time or discrete versus dense time, point in time logic versus interval logic lead to different kinds of provable properties.

A (model of a) system may be composed by components whose time modelisations and synchrony assumptions are different. Their level of description may also differ. Verification techniques for those systems should thus be scalable along time and space axis [AH96].

Among properties of particular intererest to us, the tuning of components is one of the most important. Components off the shelves must usually be tuned/adapted before being integrated in a system [BBRR97,BR97].

As a scholarly example of tuning let's consider the classical Fischer's real-time mutual exclusion protocol for two processes P₁ and P₂ :

  Pi :
		repeat
				repeat
						await k = 0
						k := i; delay b
				until k = i
				CSi
				k := 0
		forever

Variable k is shared between the processes and is initially set to 0. Exclusive access to their respective critical section then relies on two parameters : the delay b and the time a it takes a process to write a value in a variable. To complicate matters, the processes use drifting clocks, P₁'s being slow and P₂'s being fast.

Figure 3 presents the behavior of the P_i's in the hybrid automaton formalism [AD94,Hen96]. The clocks' speeds are x and y.

  

Figure 3: Fischer's mutual exclusion protocol

HyTech [HHW97] verification's algorithm on the automata of figure 3 gives the condition 8b > 11a for the safety property P₁ and P₂ are never in their critical section at the same time to be true.

Formal descriptions should be modular. However correct modules/components can be connected so that the overall behavior is no more correct as illustrated by the following example. This example is taken from [SY96]. A medium receives messages from a sender and transmits them to a receiver. Two consecutive inputs are separated by 7 units of time, two consecutive outputs are separated by at least 4 units of time, and the transmission delay between an input and an output in is the interval [3,8]. See figure 4. If the delay interval is replaced with ]7,8], a deadlock occurs in ABD with clocks x and z equal to 7 : time cannot progress and out is not enabled.

  

Figure: A channel modelisation [SY96]

Fortunately some techniques exist to detect if an hybrid automaton is non Zeno [HNSY94].

Composition schemas of hybrid automata rely heavily on when transitions of the composed automaton will be permitted to fire. Let [l_A,u_A] and [l_B,u_B] be the bounds associated with two transitions of automata A and B. The bounds on the corresponding transition of the composed automaton could be $[\max\{l_A,l_B\},\min\{u_A,u_B\}]$ or $[\max\{l_A,l_B\},\max\{u_A,u_B\}]$ or $[\min\{l_A,l_B\},\min\{u_A,u_B\}]$. Depending on the choice, properties may or may not be verified on the composed system. It remains to understand the semantics of such composition schemas. As noted in [SY96], when composing timed systems, three independent parameters operate :

Can we exhibit rules for choosing a particular composition schema ?

A related question is : ``can we exhibit a sufficiently powerful execution model to describe behaviors ?''. For instance the partially ordered multiset of events execution model of Pratt [Pra86] is used in the executable architectural description language Rapide [LKA⁺95] and many applications were claimed to be simulated with it. However we were not able to use this model to describe the famous train-gate controller problem [HL94], due to the inability of the model to test and discard time valued events.

Another question has to do with the various formalisms that can be used to describe independantly developped components. How can those formalisms interoperate in a common framework when they are integrated in the complete application's model ? Synchronous languages like ESTEREL [BG92] and LUSTRE [HCRP91], despite having completly different execution models, rely on a common intermediate formalism, which permits components developped in those two different languages to interoperate at the level of their execution.