A Compared Study of Two Correctness Proofs for the Standardized Algorithm of ABR Conformance.
The ABR conformance protocol is a real-time program that controls dataflow rates on ATM networks. A crucial part of this protocol is the dynamical computation of the expected rate of data cells. We present here a modelling of the corresponding program with its environment, using the notion of (parametric) timed automata. A fundamental property of the service provided by the protocol to the user is expressed in this framework and proved by two different methods. The first proof relies on inductive invariants, and was originally verified using theorem-proving assistant COQ. The second proof is based on reachability analysis, and was obtained using model-checker HYTECH. We explain and compare these two proofs in the unified framework of timed automata.
Introduction
Over the last few years, an extensive amount of research has been devoted to the
formal verification of real-time concurrent systems. Basically, formal proof methods
belong to two different fields: theorem proving and model-checking. For all
these methods, a first crucial phase is to build a formal description of the system
under study. With theorem proving, the description consists of a set of formulas,
and the verification is done using logical inference rules. With model-checking,
the description is a graph and the verification is performed using systematic
search in the graph. The theorem-proving methods apply to more general prob-
lems, but often need human interaction while model-checking methods are more
mechanical, but apply to a restricted class of systems. These methods thus appear
as complementary ones, and several authors advocated for the need to
combine them together [17, 21, 24]. This is now an exciting and ambitious trend
of research, but still a very challenging issue. We believe that a preliminary useful
step towards this objective is to evaluate comparatively the respective merits
Partially supported by Action FORMA (French Programme DSP-
STTC/CNRS/MENRT) and RNRT Project Calife
and shortcomings of such methods, not only at a general abstract level, but on
difficult practical examples. From such a comparison, one may hopefully draw
some general lessons for combining methods in the most appropriate way. Besides
the comparison may be interesting per se, as it may contribute to a better
understanding of the specific treated problem. We illustrate here the latter point
by performing a compared analysis of two correctness proofs obtained separately
for a sophisticated real-life protocol.
More precisely, we propose a comparison between two proofs of the Available
Bit Rate (ABR) conformance algorithm, a protocol designed at France Telecom
[15] in the context of network communications with Asynchronous Transfer
Mode (ATM). The first proof [19, 18] was obtained in the theorem proving frame-work
using Floyd-Hoare method of inductive invariants and the proof assistant
Coq [7]. The second proof [8] was based on the method of reachability analysis,
and used the model-checking tool HyTech [14]. In order to compare these methods
more easily, we formulate them in the unified framework of "p-automata"
[8], a variant of parametric timed automata [5]. The choice of such a framework
(motivation, differences with other models, specific problems) is discussed at the
end of the paper (section 7).
Context and motivation of the case study. ATM is a flexible packet-switching
network architecture, where several communications can be multiplexed
over a same physical link, thus providing better performances than traditional
circuit-switching networks. Several types of ATM connexions, called ATM
Transfer Capabilities (ATC), are possible at the same time, according to the
dataflow rate asked (and paid) for by the service user. Each mode may be seen
as a generic contract between the user and the network. On one side, the network
must guarantee the negociated quality of service (QoS), defined by a number of
characteristics like maximum cell loss or transfer delay. On the other side, data
packets (cells) sent by a user must conform to the negociated traffic parameters.
Among other ATCs, Deterministic Bit Rate connexions operate with a constant
rate, while Statistical Bit Rate connexions may use a high rate, but only for
In some of the most recently defined ATCs, like Available Bit Rate (ABR),
the allowed cell rate (Acr) may vary during the same session, depending on the
current congestion state of the network. Such ATCs are designed for irregular
sources, that need high cell rates from time to time, but may reduce their cell
rate when the network is busy. A servo-mechanism is then proposed in order to
let the user know whether he can send data or not. This mechanism has to be
well defined, in order to have a clear traffic contract between user and network.
The conformance of cells sent by the user is checked using an algorithm called
GCRA (generic control of cell rate algorithm). In this way, the network is protected
against user misbehaviors and keeps enough resources for delivering the
required QoS to well behaved users. In fact, a new ATC cannot be accepted (as
an international standard) without an efficient conformance control algorithm,
and some evidence that this algorithm has the intended behavior.
In this paper, we study the particular case of ABR, for which a simple "ideal"
algorithm of conformance control can be given. This algorithm is very inefficient,
in terms of memory space, and only approximation algorithms can be implemented
in practice. The correctness proof for these approximation algorithms
consists in showing that their outputs are never smaller than the outputs computed
by the ideal algorithm. More precisely, we focus on an algorithm, called
due to Christophe Rabadan at France-Telecom, now part of the I.371.1 standard
[15]. We describe this algorithm and prove its correctness with respect to
the ideal algorithm, using the two methods mentioned above.
The plan of the paper is as follows: section 2 gives an informal description of
the problem of ABR conformance control and section 3 presents an incremental
algorithm used henceforth as a specification. Section 4 describes a general modelling
framework, called "p-automata", and expresses the two different proof
methods in this context; the description of ABR algorithms as p-automata is
given in section 5. Verification with the two proof methods is done in section 6.
A discussion on constraints linked to the modelling with p-automata follows in
section 7, then a comparison between the two methods is given in section 8. We
conclude in section 9.

Overview

of ABR
update
DGCRA
resource management cell
user network
ACR
data cell
Fig. 1. conformance control
An abstract view of the ABR protocol is given in Figure 1. The conformance
control algorithm for ABR has two parts. The first one is quite simple and is not
addressed here. It consists of an algorithm called DGCRA (dynamic GCRA),
which is an adaptation of the public algorithm for checking conformance of
cells: it just checks that the rate of data cells emitted by the user is not higher
than a value which is approximately Acr, the allowed cell rate. Excess cells may
be discarded by DGCRA. In the case of ABR, the rate Acr depends on time:
its current value has to be known each time a new data cell comes from the
user. Thus, the complexity lies in the second part: the computation of Acr(t)
("update" in Figure 1), where t represents an arbitrary time in the future, at
which some data cell may arrive. The value of Acr(t) depends on successive values
carried by resource management (RM) cells transmitted from the network to the
user 1 . Each such value corresponds to some rate Acr, that should be reached as
soon as possible.
2.1 Definition of ideal rate Acr(t)
We consider the sequence of values (R carried by RM cells, ordered
by their arrival time (r i). By a slight abuse of notation, the cell
carrying R i will be called . The value Acr(t) depends only on cells R i
whose arrival time r i occur before t. Intuitively, Acr(t) should be the last value
R i received at time t, i.e. Rn with ug.
Unfortunately, because of electric propagation time and various transmission
mechanisms, the user is aware of this expected value only after a delay. Taking
the user's reaction time - observed by the control device into consideration, that
is, the overall round trip time between the control device and the user, Acr(t)
should then be Rn with may vary in turn. ITU-T considers
that a lower bound - 3 and an upper bound - 2 for - are established during the
negociation phase of each ABR connection. Hence, a cell arriving from the user
at time t on DGCRA may legitimately have been emitted using any rate R i
such that i is between last(t rate less than or equal to
any of these values, or, equivalently less than or equal to the maximum of them,
should then be allowed. Therefore, Acr(t) is taken as the maximum of these R i .
are the successive arrival times of RM
cells, such that :
(in other words,
depend on t) and if Rm ; are the corresponding rate values, then
the expected rate is
The case where obtained when no new RM cell has arrived between
A program of conformance control based on this specification would need
to compute, at each instant s, the maximum of the rate values of all the RM
Actually, RM cells are sent by the user, but only their transmission from the network
to the user is relevant here; details are available in [22]
cells received during interval which may be several hundreds on an
ATM network with large bandwidth. ITU-T committee considered that an exact
computation of Acr(t) along these lines is not feasible at reasonable cost with
current technologies.
2.2 Algorithm efficient computation of an approximation of
A more realistic algorithm, called due to C. Rabadan, has been proposed by
France-Telecom and adopted in I.371.1. It requires the storage of no more than
two RM cell rates at a time, and dynamically computes an approximation value
A of Acr(t). Two auxiliary variables, Efi and Ela, are used in the program for
storing these two RM cell rates and two dates, tfi and tla, are associated with
Efi and Ela respectively. When the current time s reaches tfi, A is updated with
value Efi, and only one RM cell rate is kept in memory (Efi:=Ela, tfi:=tla).
When a new RM cell arrives auxiliary variables Efi, Ela, tfi and tla
are updated according to several cases, depending on the position of r k w.r.t.
tfi and tla, and R k w.r.t. Efi and Ela. The full description of B 0 is given in
section 5.3 (cf. pseudocode in appendix A).
Correctness of B 0 . Before being accepted as an international standard (norm
ITU I-371.1), algorithm B 0 had to be proved correct with respect to Acr(t): it
was necessary to ensure that the flow control of data cells by comparison with A
rather than Acr(t) is never disadvantageous to the user. This means that when
some data cell arrives at time t, A is an upper approximation of Acr(t).
3 Incremental computation of the rate Acr(t)
As explained above, the correctness of algorithm B 0 mainly relies on a comparison
between the output value A of B 0 and the ideal rate Acr(t). The initial
specification of Acr(t) given in section 2.1, turns out to be inadequate for automated
(and even manual) manipulation. Therefore, it is convenient to express
the computation of Acr(t) under an algorithmic form as close as possible to B 0 ,
where, in particular, updates are performed upon reception of RM cells. Monin
and Klay were the first to formulate such an incremental computation using a
higher-order functional point of view [19]. We recall their algorithm, then adopt
a slightly different view, which is more suited to the modelling framework described
subsequently.
3.1 A higher-order functional view: algorithm F
We now consider an algorithm, called F , that stores, at current time s, an
estimation E of Acr, and updates it at each arrival of an RM cell. More precisely,
when receiving a new cell R k at time r k , algorithm F computes the new function
0 from the former function E, depending on the situation of r k with respect to
the argument t of E:
It can be shown that the value E(t) at current time s is equal to the ideal
rate Acr(t), as defined in section 2.1, for each t such that t - s
proof of this statement can be found in [19], although a much shorter one can
be deduced from the justification in section 3.2 below.
Algorithm F can thus be seen as a higher order functional program which
computes the (first-order) functions E. It might be implemented using the general
notion of "closures". However, the functions E are constant over time intervals
[a; b[, where a and b are of the form r and such that there is no value
of this form between a and b. Hence, they can be encoded using well chosen
finite lists of pairs (t; e), where t is a time and e is the rate E(t). Such lists
can be seen as schedulers for the expected rate: when current time s becomes
equal to t, the expected rate becomes e. The length of these schedulers may be
several hundreds on networks with large bandwidth (entailing a high frequency
of events R k ), even if only the relevant pairs (t; e) are kept. In contrast, algorithm
can be considered as using a scheduler of length at most two (containing pairs
(tfi,Efi), (tla,Ela)).
3.2 A parametric view: algorithm I t
Another way of looking at F is to consider t as a parameter (written t) whose
value is fixed but unknown, and represents a target observation time. Function F
becomes an "ideal algorithm" I t
, which updates a value E(t), henceforth written
, upon reception of RM cells as follows:
It is now almost immediate that the value E t
computed by I t
, is equal to the
ideal rate Acr(t), as defined in section 2.1, when t. Indeed, as s increases,
k takes the values
with
takes accordingly the values
In particular, when t, we have E t
The correctness property of B 0 with respect to Acr(t) can now be reformulated
as follows, where A is the output value of B 0 and E t the value computed by
algorithm I t
when
This property is referred to as U t and should be proved for all values of parameter
t. Henceforth, the parameter t is left implicit and we simply write U instead
of U t . Accordingly, we write E instead of E t and I instead of I t . From this point
on, algorithm I plays the r-ole of specification.
Modelling Framework and Proof Methods
It should be clear from the informal definition of the control conformance algorithm
above, that the ability to reason about real time is essential. The
expressions A and E, involved in property U , denote quantities that evolve as
time goes, and should be considered as functions of the current time s. In order
to express and prove property U , we need a formal framework. The model of
p-automata which was chosen in this paper, turns out to be sufficient for our
purposes of formal description and verification of the considered system. We describe
this model hereafter as well as two proof methods for verifying properties
in this context.
4.1 p-automata
The model of parametric timed automata, called p-automata for short, is an
extension of timed automata [4] with parameters. A minor difference with the
classical parametric model of Alur-Henzinger-Vardi [5] is that we have only one
clock variable s and several "discrete" variables w 1 ; :::; wn while, in [5], there are
several clocks and no discrete variable. One can retrieve (a close variant of) Alur-
Henzinger-Vardi parametric timed automata by changing our discrete variable w
into s\Gammaw i (see [12]). Alternatively, p-automata can be viewed as particular cases
of linear hybrid automata [2, 3, 20], and our presentation is inspired from [14].
The main elements of a p-automaton are a finite set L of locations, transitions
between these locations and a family of real-valued variables. In the figures, as
usual, locations are represented as circles and transitions as labeled arrows.
Variables and constraints. The variables of a p-automaton are: a tuple p
of parameters, a tuple w of discrete variables and a universal clock s. These
real-valued variables differ only in the way they evolve when time increases.
Parameter values are fixed by an initial constraint and never evolve later on.
Discrete variable values do not evolve either, but they may be changed through
instantaneous updates. A universal clock is a variable whose value increases
uniformly with time.
A (parametric) term is an expression of the form w+ \Sigma i ff
or \Sigma i ff are
constants in Z. With the usual convention, an empty set of indices corresponds
to a term without parameter. A convex constraint is a conjunction of (strict
or large) inequalities between terms. A p-constraint is a disjunction of convex
constraints. An update relation is a conjunction of inequalities between a variable
and a term. It is written w 0 fi term, where w 0 is a primed copy of a discrete
variable and term is a parametric term. As usual, x
is implicit if x 0 does not appear in the update relation.
Locations and transitions. With each location ' 2 L is associated a convex
constraint called location invariant. Intuitively, the automaton control may reside
in location ' only while its invariant value is true, so invariants are used to enforce
progress of the executions. When omitted, the default invariant of a location is
the constant true.
A transition in a p-automaton is of the form: h'; '; a; '; ' 0 i, where a is the
label of the transition, ' the origin location, ' 0 the target location, ' a guard and
' an update relation. The guard is a convex constraint. Guards may additionnaly
contain the special expression asap. In our model, a location ' is called urgent
if all transitions with origin ' contain asap in the guard (no time is allowed
to pass in such a location). Otherwise, it is called stable. A sequence of transitions
is called complete if it is of the form h';
are stable locations and all intermediate
locations ' i are urgent locations. With the usual convention, the case
corresponds to a single transition between stable locations.
Executions. The executions of a p-automaton are described in terms of a transition
system. A (symbolic) state q is defined by a formula (- /(s; p; w),
where - is a variable ranging over the set of locations, and / is a p-constraint.
We are primarily interested in states for which / implies the location invariant
I ' . Such states are called admissible states. A p-zone, represented by a formula
\Pi(-; s; p; w), is a finite disjunction of states. Alternatively it can be regarded
as a finite set of states. The initial state is q init
some p-constraint / init and initial location ' init . Initial location is assumed to
be stable. Since parameter values are fixed from the initial state, we often omit
the tuple p of parameters from the formulas. For a p-automaton, two kinds of
moves called action moves and delay moves are possible from an admissible state
- An action move uses a transition of the form h'; '; a; '; ' 0 i, reaching an admissible
state
equivalent to 9w /(s; w) - '(w; w 0 ). Informally, discrete variables are modified
according to update relation ' and the automaton switches to target
location ' 0 . This notion of action move generalizes in a natural way to the
notion of action move through a complete sequence of transitions. Note that
action moves are instantaneous: the value s of the clock does not evolve.
- A delay move corresponds to spending time in a location '. This is possible
if ' is stable and if the invariant I ' remains true. The resulting admissible
state is q (nothing else is changed during
this time).
A successor of a state q is a state obtained either by a delay or an action
move. For a subset Q of states, P ost   (Q) is the set of iterated successors of the
states in Q. It can be easily proved that the class of p-zones is closed under
the P ost operation. As a consequence, P ost   (Q) is a p-zone if Q is a p-zone
and computation of P ost   terminates. The notion of predecessor is defined in a
similar way, using operator P re.
Synchronization. From two or more p-automata representing components of a
system, it is possible to build a new p-automaton by a synchronized product. Let
A 1 and A 2 be two p-automata with a common universal clock s. The synchronized
product (or parallel composition, see e.g. [14]) A 1 \Theta A 2 is a p-automaton
with s as universal clock and the union of sets of parameters (resp. discrete
variables) of A 1 and A 2 as set of parameters (resp. discrete variables). Locations
of the product are pairs of locations from A 1 and A 2 respectively. A
are stable. The p-constraints associated with
locations (invariants, initial p-constraint) are obtained by the conjunction of
the components p-constraints. The automata move independently, except when
transitions from A 1 and A 2 have a common synchronization label. In this case,
both automata perform a synchronous action move, the associated guard (resp.
update relation) being the conjunction of both guards (resp. update relations).
4.2 Proof methods
We now present two proof methods for proving a property \Pi(-; s; w) in the
framework of p-automata. This property is assumed to involve only stable loca-
tions, and to hold for all parameter valuations satisfying the initial p-constraint
of the modeled system. The first method, based on Floyd-Hoare method of as-
sertions, consists in proving that \Pi is an inductive invariant of the model (see,
e.g., [27]). The second one, based on model-checking techniques, consists in characterizing
the set of all the reachable states of the system, and checking that no
element violates \Pi.
Inductive invariants. To prove \Pi by inductive invariance, one has to prove
that \Pi holds initially, and is preserved through any move of the system: either
an action or a delay move. Formally, we have to prove:
- For any transition h'; '; a; '; ' 0 i between two stable locations ' and
A similar formula must also be proved for complete sequences of transitions.
- For any stable location ':
I ' (s; w) - I ' (s
Reachability analysis. Since P ost   (q init ) represents the set of reachable states
of a p-automaton, property \Pi holds for the system if and only if P ost   (q init )
is contained in the set Q \Pi of states satisfying \Pi. Equivalently, one can prove
the emptiness for the zone P ost   (q init is the set of states
violating \Pi. Also note that the same property can be expressed using P re   by
re   (Q:\Pi
5 Description of the system
Algorithms I and B 0 will be naturally represented by p-automata. However, they
are reactive programs: they react when some external events occur (viz., upon
reception of an RM cell) or when current time s reaches some value (e.g., tfi).
Thus, in order to formally prove correctness property U , we need to model as a
third p-automaton, an appropriate environment viewed as an event generator.
Finally, in the full system obtained as a synchronized product of the three au-
tomata, we explain how to check the correctness property. All these p-automata
share a universal clock s, the value of which is the current time s. Without loss
of understanding (context will make it clear), we often use s instead of s.
5.1 A model of environment and observation
As mentioned above, the p-automaton A env modeling environment (see Figure 2)
generates external events such as receptions of RM cells. It also generates a
"snapshot" action taking place at time t. Note that for our purpose of verification
of U , it is enough to consider the snapshot as a final action of the system. The
variables involved are the parameter t (snapshot time) and a discrete variable
R representing the rate value carried by the last received RM cell. In the initial
location W ait, a loop with label newRM simulates the reception of a new RM
cell: the rate R is updated to a non deterministic positive value (written R' ? 0,
as in HyTech [14]). The snapshot action has s=t as a guard, and location W ait
is assigned invariant s - t in order to "force" the switch to location EndE.
Wait
newRM
R
snapshot
Fig. 2. Automaton Aenv modeling arrivals of RM cells and snapshot
5.2 Algorithm I
Algorithm I computes E in an incremental way as shown in the table of section
3.2. Variable E is updated at each reception of an RM cell, until current
time s becomes equal to t. More precisely, algorithm I involves variable R and
parameter t (in common with A env ) and, in addition:
- the two parameters - 3 and - 2 (representing the lower and upper bounds of the
transit time from the interface to the user and back),
- the "output" variable E (which equates with the ideal rate Acr(t) when
Initially, E and R are equal. Algorithm I reacts to each arrival of a new RM cell
with rate value R by updating E. There are three cases, according to the position
of its arrival time s with respect to t- 2 and t- 3 (see section 3.2):
1. If s - t- 2 , E is updated to the new value R:
2. If t- the new rate becomes E'=max(E,R). To avoid using
function max, this computation is split into two subcases:
3. If s ? t- 3 , the rate E is left unchanged:
Algorithm I terminates when the snapshot takes place (s=t). In the following,
we will sometimes write the updated output value E' under the ``functional''
form I(s; R; E).
Automaton AI . Algorithm I is naturally modeled as p-automaton A I (see

Figure

3). Initial location is Idle, with initial p-constraint R. The reception
of an RM cell is modeled as a transition newRM from location Idle to location
UpdE. This transition is followed by an urgent (asap) transition from UpdE back
to Idle, which updates E depending on the position of s w.r.t. t- 2 and t- 3 ,
as explained above. Without loss of understanding, transitions from UpdE to
Idle are labeled [I1], [I2a], [I2b], [I3] as the corresponding operations.
Observation of the value E corresponds to the transition snapshot from Idle to
final location EndI.
5.3 Algorithm computation of an approximation
We now give a full description of algorithm B 0 (cf. pseudo-code in appendix).
Like I, algorithm B 0 involves parameters - 3 and - 2 and variable R. However, note
that t is not a parameter for B 0 . It computes A (intended to be an approximation
of E) using five specific auxiliary variables:
- tfi and tla, which play the role of fi-rst and la-st deadline respectively,
- Efi, which is the value taken by A when current time s reaches tfi,
- Ela, which stores the rate value R carried by the last received RM cell.
- Emx, a convenient additional variable, representing the maximum of Efi, Ela.
Initially, s=tfi=tla, and the other variables are all equal. Algorithm B 0 reacts
to two types of events: "receiving an RM cell" (which is an event in common
with I), and "reaching tfi" (which is an event specific to B 0 ).
Idle
snapshot
newRM
[I3]
Fig. 3. Automaton AI
Receiving an RM cell. When, at current time s, a new RM cell with value R
arrives, the variables are updated according to the relative positions of s+- 3
and s+- 2 with respect to tfi and tla, and those of R with respect to Emx
and A. There are eight cases from [1] to [8] (with two subcases for [1]):
[3] if s ! tfi and Emx != R and tfi ?= s+- 3 and A != R then
[6] if s ! tfi and Emx ? R and R ?= Ela then
[8] if s ?= tfi and A ? R then
Reaching tfi. When the current time s becomes equal to tfi, the approximate
current rate A is updated to Efi while Efi is updated to Ela and tfi
is updated to tla (operation [9]):
When the events "reaching tfi" (s=tfi) and "receiving an RM cell" simultaneously
occur, operation [9] must be performed before operation [1], ., [8]
(accounting for the RM cell reception).
Like I, algorithm B 0 terminates at snapshot time (s=t). If the snapshot occurs
simultaneously with reaching tfi, operation [9] must be performed before
termination of B 0 .
Note that the ordering of s, tfi and tla just after operation [9] depends on
the respective positions of tfi and tla at the moment of performing [9]. In case
(s=)tfi=tla, one still has s=tfi=tla just after performing [9], then s becomes
greater than tfi=tla as time increases (until an RM cell occurs or s=t). In case
(s=)tfi!tla when performing [9], one has s!tfi=tla immediately after.
Automaton AB 0 . In order to implement the higher priority of operation [9]
over the other operations in case of simultaneous events, it is convenient to
distinguish the case where s is greater than tfi from the case where s-tfi. To
that goal, we introduce two locations Greater and Less. Operation [9] always
occurs at location Less, but the target location depends on whether tfi=tla
(subcase [9a]) or tfi!tla (subcase [9b]).
The p-automaton AB 0 is represented in Figure 4 with only the most significant
guards and no update information. Like before, the same labels are used for
automaton transitions and corresponding program operations.
Less
Greater
UpdAL
UpdAG
s=tfi!tla
snapshot
snapshot
s=tfi=tla
newRM
asap
or [8]
newRM
asap
[1] or [2] or ::: or [6]
Fig. 4. Approximation automaton AB 0
Initially AB 0 is in Greater, with p-constraint: s=tfi=tla - A=Efi=Ela=Emx=R.
Location Less has s-tfi as an invariant, in order to force execution of transition
(if tfi!tla) or [9a] (if tfi=tla) when s reaches tfi. From Less, transition
goes back to Less (since, after update, s!tfi=tla) while transition
[9a] switches to Greater (since s-tfi=tla as time increases). The reception
of an RM cell corresponds to a transition newRM . There are two cases depending
on whether the source location is Less or Greater. From Less (resp.
Greater), transition newRM goes to location UpdAL (resp. UpdAG). This transition
is followed by an urgent transition from UpdAL (resp. UpdAG) back to
Less, which updates the discrete variables according to operations [1],.,[6]
(resp. [7],[8]), as explained above. Note that transition newRM from Less
to UpdAL has an additional guard s!tfi in order to prevent an execution of
newRM before [9a] or [9b] when s=tfi (which is forbidden when "reaching
tfi" and newRM occur simultaneously).
Like before, observation is modeled as a transition snapshot from location
Less or Greater to EndB. Also note that transition snapshot from Less to
EndB has guard s!tfi in order to prevent its execution before [9a] or [9b]
when s=tfi (which is forbidden when "reaching tfi" and the snapshot occur
simultaneously).
5.4 Synchronized product and property U
The full system is obtained by the product automaton I \Theta AB 0 of
the three p-automata above, synchronized by the labels newRM and snapshot.
The action moves occur when the current time reaches tfi or t or upon reception
of an RM cell (newRM ). In this last case, return to a stable location is
obtained by a complete sequence of transitions: newRM followed by transitions
[I1],[I2a],[I2b],[I3] in A I and [1],.,[6] or [7],[8] in AB 0 .
Recall that property U expresses in terms of the ideal rate E computed by
I, and the approximate value A computed by B 0 , as: when In
our model T , snapshot action occurs as soon as s=t, and makes the automaton
switch to its final location Henceforth we
respectively for locations (W ait; Idle; Greater) and (W ait; Idle; Less).
Actually, the property A - E does not hold in all locations of T when s=t. This is
due to the necessary completion of all the actions in case of simultaneous events.
Thus, at location ' \Gamma , when s=t=tfi, one may have A ! E just before treatment
of [9]. However in location ' all the appropriate
actions are completed. Property U states therefore as follows:
Since location ' 1 is reached when s=t, and no action then occurs, an equivalent
statement of U is:
6 Verification of correctness
6.1 Verification with inductive invariants
In order to prove U E, we are going to prove that Inv j U -
is an inductive invariant of the system, where Aux i are auxiliary properties
of the system. Some of these auxiliary properties (viz., Aux 3
involve an additional variable r, which represents the reception date of the last
RM cell. (Such variables, that record some history of system execution without
affecting it, are called "history" variables [1, 27].) In our model, this can be easily
implemented by introducing a discrete variable r in the environment automa-
ton, and updating it with current time value s, whenever event newRM occurs.
. Enriched automaton A env is represented in Figure 5.
Wait
newRM
R
snapshot
Fig. 5. Enriched automaton Aenv modeling arrivals of RM cells and snapshot
More precisely, let Aux
proved by inductive invariance, i.e. by showing
that it holds initially and is preserved through any transition corresponding
to either a complete action move or a delay move. The stable locations are '
. The action moves starting from and leading to one of these locations
are those associated with the reception of an RM cell, the reaching of tfi, or
snapshot. In the case of RM cell reception, there are several subcases depending
on the complete sequence of actions in AB 0 (newRM followed by [1a], [1b],
and, subsidiarily, on the sequences in A I (newRM followed
by [I3]g). We now give in details the statements involved in the
proof. Variables of Inv are explicitly mentionned by writing Inv(-; s;
w is the vector (E, Efi, Ela, Emx, A, R, tfi, tla). Note that, provided an
encoding of locations given as integers (e.g., 0; 1; 2), all these statements
are linear arithmetic formula over reals (involving variables -; s;
can be proved just by arithmetic reasoning. This can be done automatically
with an arithmetic theorem prover. Such a proof was actually done using Coq
[18], then was reformulated in the present context, after encoding p-automata in
Coq. Let us recall that, in Coq, the user states definitions and theorems, then
he proves the latters by means of scripts made of tactics. Scripts are not proofs,
but produce proofs, which are data (terms) to be checked by the kernel of the
proof assistant. Some tactics used for ABR were described in [18]. The script
written for the ABR is about 3500 lines long and required about 4 man-months
of work. A crucial part of the human work consisted in identifying the relevant
invariants. Around two hundred subproofs were then automatically produced
and checked. The whole proof check takes 5 minutes on a PC 486 (33 MHz)
under Linux.
In order to give a flavour of the proof structure, we give now some typical
statements to be proved in the case of action and delay moves.
Action moves. As an example, consider the reception of an RM cell where the
subsequent action of AB 0 is [1b]. This corresponds to a complete sequence of
transitions from location ' \Gamma to itself. We have to prove:
E)
The conclusion conjunction of the
9
tla
For example, let us show how to prove Aux 0
9 , i.e. E
assuming tfi -
. By Aux 10 , we have E - Ela (since tla - t). By Aux 8 , we have
Ela - Efi (since tfi=tla). Hence, by transitivity: E- Efi. On the other hand,
E'=E by [I3] (since
(= tla
All the other cases
are proved similarly to this one, by case analysis, use of transitivity of -; !; =,
and regularity of + over these relations.
Delay moves. They take place at stable locations ' . The corresponding
properties to be proved are respectively:
These formula easily reduce to:
The first (resp. second, third) implication is true because its conclusion A - E
follows from the hypothesis using the Aux 1 -conjunct (resp. Aux 2 -conjunct, U -
conjunct) of Inv.
6.2 Verification by reachability analysis
In order to mechanically prove property U , we have to compute P ost   for the
product automaton T , starting from its initial state
where / init is the p-constraint s=tfi=tla - R=E=A=Efi=Ela=Emx- 0!- 3 !- 2 .
We then have to check that P ost   (q init ) does not contain any state where the
property U is violated. Recall that property U can be stated as:
The state where U does not hold is then
Automata A env , A I and AB 0 can be directly implemented into HyTech [14],
which automatically computes the synchronized product T . The modelling of
the protocol and property as p-automata and the encoding in Hytech required
about 3 man-months of work. The forward computation of P ost   (q init ) requires
iteration steps and its intersection with q :U is checked to be empty. (This
takes 8 minutes on a SUN station ULTRA-1 with 64 Megabytes of RAM memory.

Appendix

B for a display of the generated p-zone at ' 1 . ) This achieves an
automated proof of correctness of B 0 . Such a proof first appears along these lines
in [8]. Note that HyTech can provide as well a proof by backward reasoning
(using P re   instead of P ost   ).
7 Discussion on p-automata
Tools based on timed automata have been successfully used in the recent past for
verifying or correcting real-life protocols (e.g., the Philips Audio Control protocol
[16] and the Bang & Olufsen Audio/Video protocol [13]). Experiences with such
tools are very promising. This observation led us to use here p-automata, a close
variant of timed automata. The differences between p-automata and classical
timed automata are two-fold. A first minor difference is that p-automata use a
form of "updatable" time variables instead of traditional clocks (but see [9] for
a proof of equivalence between the two classes). Second p-automata incorporate
parameters, which are essential in our case study. The choice of Hytech, as an
associated tool, is natural in this context. We now explain some new features
that appear in the proof of the protocol using p-automata, and some difficulties
encountered in the process of building the specification.
7.1 Towards p-automata
We first point out some significant differences between the proof by invariants as
stated by Monin and Klay [19, 18] and the corresponding proof presented here
(see section 6.1).
Representation of time. In the work reported in [19, 18], the formalization of
time aspects, though influenced by timed automata, was performed using ad hoc
devices, appealing to the reader's natural understanding. This problem is settled
here, thanks to p-automata, which include a built-in notion of clock and rely on
a well-understood and widely accepted notion of time. The use of p-automata,
although it introduces an additional level of encoding, thus makes the effort
of specification easier with this respect. Note however that the encoding of p-
automata in Coq does not specify a priori the granularity of time evolution, and
allows for either a continuous or discrete underlying model of time. It is based on
a minimal underlying theory of arithmetic (mainly the transitivity of relations
!; - and the regularity of + over them). This is not the case in the theory of
timed automata and the associated tools like Hytech (or others [6, 11]) where
the time domain is assumed to be continuous (Q or R), and a sophisticated
package for manipulating linear constraints over real arithmetic is used. We will
come back to this difference (see section 8.2).
Higher-order vs. first-order specifications. As recalled in section 3, Monin
and Klay [19] introduced an incremental way of computing the ideal rate Acr(t)
(higher-order algorithm F). We then recast their algorithm F under a parametric
form I. The latter view is probably less natural, but fits better into the first order
framework of p-automata.
Reformulating the proof by invariance. We also rewrote the proof by invariance
of [19] in the context of p-automata, in order to assess the proofs in
a uniform framework. Expressing the auxiliary properties needed in this proof
required to (re)introduce history variable r accounting for the reception time
of the last RM cell. Moreover, these properties only concerned stable locations
of the system: expressions of the form had to be included, and only
complete sequences of actions were considered. Note that the auxiliary property
is different from its counterpart Aux 0
as found in [19]. Actually, Aux 0
8 is false in our model.
We will subsequently explain this discrepancy (see section 8.2).
7.2 Specific modelling problems with p-automata
In the process of constructing p-automata while keeping with the specification,
we had to face some problems, which are listed below.
Modelling the environment as a p-automaton. In addition to the automata
corresponding naturally to I and B 0 , a third automaton was introduced
to model the environment, thus providing a clear separation between external
and internal events.
Introducing urgent locations. The class of update relations in p-automata
(derived from HyTech) does not allow for simultaneous updates. For instance,
choosing (at random) a new identical value of R and E (with an instruction like
E'=R'?0) is forbidden. In order to implement such an update relation, an urgent
intermediate location, such as UpdE depicted in figure 6, had to be introduced.
Idle
asap
update
R
newRM
instead of
Idle
newRM
Fig. 6. Reception and update with two locations instead of one
Introducing two stable locations. In order to implement the higher priority
of operation "reaching tfi" (when occuring simultaneously with other actions of
the system), we were led to create two stable locations (Greater and Less) in the
p-automaton representing algorithm B 0 . Note that we overlooked this priority
requirement in a preliminary implementation embedding only one stable loca-
tion, which entailed a violation of property U . (This was detected subsequently
by running HyTech.)
8 Proof Comparison
We now assess the respective merits and shortcomings of the proof methods by
invariance and reachability analysis within the unified framework of p-automata,
regarding the ABR conformance problem. We also explain how to cross-fertilize
the results of the two methods.
8.1 Automated proof vs. readable proof
It is well-known that a proof in a model-checker is more automatic, but that more
insight in the algorithm is gained by doing the proof with a theorem-prover. Let
us confirm this general opinion in our particular case study.
As already noticed, the reachability proof was done in a fully automatic manner
(via HyTech). This is an outstanding advantage over the proof by inductive
invariance (which required the human discovery of several nontrivial auxiliary
properties) and justifies a posteriori our effort of translating the problem into the
formalism of p-automata. In particular, it becomes easier to validate other ABR
conformance protocols as soon as they are formalized themselves in terms of
p-automata. This is actually what was done recently in the framework of RNRT
project Calife: different variants of B 0 were easily checked (or invalidated) with
HyTech by reachability analysis along the lines described above. It was not possible
to do the same with the inductive invariance approach because several of
the original auxiliary properties became false while others had to be discovered.
Nevertheless, several qualifications must be done about this positive side of
model-checking. Let us first stress that the proof obtained by reachability analy-
sis, merely consists of a long list of constraints (see appendix B) that represents
the whole set of reachable symbolic states. This information is hardly exploitable
by a human: in particular the essential fact that such a list is complete (i.e. "cov-
ers" all the reachable states) is impossible to grasp by hand. In contrast, the
invariance proofs as checked by a theorem prover are more human-oriented. It is
instructive to inspect the case analysis that was automatically performed, and
allows the reader to be convinced of the property accurateness (or a contrario
of some flaws). Besides, the auxiliary properties are very important per se, and
bring important information about algorithm B 0 itself. (Some of these properties
are indeed part of norm ITU I.371.1, and must be henceforth fulfilled by any
new ABR algorithm candidate to normalization.)
We explain now how one can go beyond the limitations of each method, by
using both of them in a fruitful cross-fertilizing way.
8.2 Cross-fertilizing proofs
Checking the output produced by Hytech. A proof produced by Hytech,
i.e. the (finite) list P ost   of all the symbolic states reached from the initial one,
can be seen as a fixed-point associated with the set of transitions of the product
automaton. Therefore, one can verify that such a list is "complete" (covers all
the reachable states) by checking that it is invariant through action and delay
moves. This can be done, using the Coq system, exactly as explained in section
6.1. This gives of course an increased confidence in the model-checking proof. In
addition it may give new insight about the conditions on the environment that
were assumed to perform the proof: as noticed in section 7.1, in Coq, we use
a very flexible model for time, assuming only that time increases (but nothing
about its continuity). In fact, the correctness of algorithm B 0 holds even for a
discrete time modelling. Such a feature cannot not be derived from the proof of
Hytech, since it uses a priori an assumption of continuous time evolution.
Checking the invariants used in Coq. In the other way around, one can
check the correctness of the auxiliary properties
simply by asking Hytech if all the reachable states satisfy them (i.e. P ost   '
10). The answer is always "yes", which gives us another
proof of the Aux i s. Recall however that Aux 8 differs from its counterpart Aux 0in [19]:
8 is false in the p-automata model
and true in the original model of Monin-Klay (see section 7.1). This discrepancy
originates from the different ways two consecutive RM cells follow each other
in the two models. In our p-automata model, two consecutive RM cells may
arrive simultaneously while this is precluded in the model of Monin-Klay as
reception times of RM cells must form a strictly increasing sequence. The model
presented here is then more general than the original model of Monin-Klay, as it
relaxes some assumption concerning the sequence of RM cells. As a by-product,
this provides us with a better understanding of the conditions under which B 0
behaves correctly.
Finally note that the model of p-automata is flexible enough to incorporate
the assumption of strictly increasing sequences of RM cells, as used in [19]: it
suffices to use explicitly the additional variable r mentioned in section 7.1 (date
of last RM cell reception), and add guard s ? r to the newRM transition in the
environment automaton of figure 5. With such a modification, property Aux 0also becomes true in the model with p-automata.
8.3 Further experiments and foreseen limits
We thus claim that checking properties proved by one tool, using the other one,
is very fruitful. As examplified above, it may reveal possible discrepancies, which
lead in turn to discover implicit modelling assumptions. It may also of course
detect real flaws, which originate from the protocol or its modelling (although it
has not been the case here). In any case this proof confrontation helps the verification
work, and increases the confidence of the human in mechanical proofs.
One can now wonder how general are the remarks we made on this case study,
given the fact that we focused on one problem (the correctness of algorithm
used two specific tools as a theorem-prover (Coq) and a model-checker
(Hytech).
Regarding the tools, we believe that our experience with Coq and Hytech
is not specific, but can be reproduced with equivalent tools as well. We have
concrete indications in this sense. Actually, in the framework of project Calife,
Pierre Cast'eran and Davy Rouillard, from University of Bordeaux, have performed
a proof similar to the proof in Coq, using the model of p-automata
and theorem prover Isabelle [10, 25]. Concerning Hytech, we do not know
any other model-checking tool allowing for parameters but, as mentioned in appendix
C, we did some successful experiments with Gap [12], a tool based on
constraint logic programming, which works as a fixed-point engine very much as
Hytech generates P ost   .
Concerning the studied problem, the success of the proof by model-checking
comes from the fact that the computation of the P ost   computation with HyTech
had terminated. This can be considered a "lucky" event, since analysis of such
a parametric algorithm is known to be undecidable [5]. This means that computation
of P ost   does not always terminate for all p-automata. (This observation
leads us to propose, in Appendix C, an "approximate" version of B 0 , belonging
to a subclass for which P ost   is guaranteed to terminate.) Is such a termination
property preserved when considering ABR conformance algorithms other
than The answer is ambivalent. On the one hand, as already mentioned,
our model-checking experience on B 0 was successfully reused on other (relatively
close) algorithms of ABR conformance in the framework of project Calife. On
the other hand, we failed to mechanically check an algorithm of ABR conformance
of a different kind: the generic algorithm of Rabadan-Klay (see e.g. [26]).
This algorithm involves an unbounded list of N scheduled dates (instead of 2,
as in B 0 ), and cannot be modeled with p-automata due to the use of a list data
type. Even for the restricted version where N is bound to a small value, e.g:
3, in which case we get a natural model with p-automata, Hytech runs out of
memory and fails to generate P ost   .
The latter experiment recalls us some inherent limits of model-checking: if
the algorithm uses not only a finite set of numeric variables, but also unbounded
data structures (such as lists), then the verification process has to rely essentially
on classical methods of theorem-proving; this is also true when the program can
be modeled as a p-automaton, but the space of reachable symbolic states is too
big to be computed by existing model-checkers.
9 Conclusion
As a recapitulation, we believe that many useful informations about real-time
programs can be obtained without resorting to new integrated tools, when it
is possible to make a joint use of well-established theorem prover and model
checker. In our case, we gained much insight about the algorithm B 0 , and important
confidence in the proofs of correctness produced by Coq and Hytech,
basically by using the unified framework of p-automata, and cross-fertilizing the
two proofs. In particular we saw that algorithm B 0 is robust in the sense that
several underlying assumptions can be relaxed: the nature of time can be discrete
(instead of continuous); the (measured) time interval between two received RM
cells can be null. Moreover, the basic p-automata model underlying B 0 was successfully
reused for proving the correctness of some variants. To our knowledge,
it is the first time that such a compared study between theorem proving and
model checking has been performed on the same industrial problem. We hope
that this work paves the way for further experiences on real-life examples. In
the framework of project Calife, we are currently developing a two-step methodology
for verifying the quality of new services provided by telecommunication
networks, which exploits the synergy between the two proof methods: the first
step, based on model-checking, yields a p-automaton model endowed with a collection
of invariants it satisfies; in the second step, the p-automaton is recasted
under an algorithmic form better suited to the end-user, and verification is done
via a generic proof assistant, with the help of invariants.



--R

"The existence of refinement mappings"
"The Algorithmic Analysis of Hybrid Systems"
"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems"
"Automata for Modeling Real-Time Systems"
"Parametric real-time reasoning"
"UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems"


"Are Timed Automata Updat- able?"

"The Tool KRONOS"
"A Closed-Form Evaluation for Extended Timed Automata"
"A User Guide to HYTECH"
"Traffic control and congestion control in B- ISDN"
"Model-Checking for Real-Time Systems"
"Beyond model checking"
"Proving a real time algorithm for ATM in Coq"
Correctness Proof of the Standardized Algorithm for ABR Conformance.
"An Approach to the Description and Analysis of Hybrid Systems"
"A Platform for Combining Deductive with Algorithmic Verification"
L'ABR et sa conformit'e.
"A Closed-Form Evaluation for Datalog Queries with Integer (Gap)- Order Constraints"
"An Integration of Model Checking with Automated Proof Checking"

"Mechanical Verification of a Generic Incremental ABR Conformance Algorithm"
"An Introduction to Assertional Reasoning for Concurrent Sys- tems."
--TR
The existence of refinement mappings
An introduction to assertional reasoning for concurrent systems
A closed-form evaluation for Datalog queries with integer (gap)-order constraints
Parametric real-time reasoning
The algorithmic analysis of hybrid systems
The tool KRONOS
UPPAALMYAMPERSANDmdash;a tool suite for automatic verification of real-time systems
Automata For Modeling Real-Time Systems
A User Guide to HyTech
Proving a Real Time Algorithm for ATM in Coq
Hybrid Automata
Correctness Proof of the Standardized Algorithm for ABR Conformance
Automated Verification of a Parametric Real-Time Program
Mechanical Verification of an Ideal Incremental ABR Conformance
Are Timed Automata Updatable?
Beyond Model Checking
An Integration of Model Checking with Automated Proof Checking
A Platform for Combining Deductive with Algorithmic Verification
Model-Checking for Real-Time Systems
An Approach to the Description and Analysis of Hybrid Systems
Formal modeling and analysis of an audio/video protocol

--CTR
Patricia Bouyer , Catherine Dufourd , Emmanuel Fleury , Antoine Petit, Updatable timed automata, Theoretical Computer Science, v.321 n.2-3, p.291-345, August 2004
telecommunication protocols;theorem proving;model checking