Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms.
AbstractMany critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system and, then, to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems.
Introduction
Synchronous systems are distributed computer systems where there are known
upper bounds on the time that it takes nonfaulty processors to perform certain op-
erations, and on the time that it takes for a message sent by one nonfaulty processor
to be received by another. The existence of these bounds simplifies the development
of fault-tolerant systems because nonfaulty processes executing a common
algorithm can use the passage of time to predict each others' progress. This property
contrasts with asynchronous systems, where there are no upper bounds on
processing and message delays, and where it is therefore provably impossible to
achieve certain forms of consistent knowledge or coordinated action in the presence
of even simple faults [6, 13].
For these reasons, fault-tolerant systems for critical control applications in air-
craft, trains, automobiles, and industrial plants are usually based on the synchronous
approach, though they differ in the extent to which the basic mechanisms
of the system really do guarantee satisfaction of the synchrony assumption. For
example, process scheduling algorithms that can miss deadlines, buffer overflows,
and contention buses such as Ethernet can all lead to violations of the synchrony
assumption, but may be considered "good enough" in less than truly critical appli-
cations. Those applications that are truly critical, however, often build on mechanisms
that are not merely synchronous but synchronized and time-triggered: the
clocks of the different processors are kept close together, processors perform their
actions at specific times, and tasks and messages are globally and statically sched-
uled. The Honeywell SAFEbus TM [1,17] that provides the safety-critical backplane
for the Boeing 777 Airplane Information Management System (AIMS) [31,39], the
control system for the Shinkansen (Japanese Bullet Train) [16], and the Time-Triggered
Protocol (TTP) proposed for safety-critical automobile functions [21] all
use this latter approach.
A number of basic functions have been identified that provide important building
blocks in the construction of fault-tolerant synchronous systems [8, 10]; these
include consensus (also known as interactive consistency and Byzantine agree-
ment) [33], reliable and atomic broadcast [9], and group membership [7]. Numerous
algorithms have been developed to perform these functions and, because of
their criticality and subtlety, several of them have been subjected to detailed formal
[15, 23, 43] and mechanically checked [2, 26-28, 34] verifications, as have their
combination into larger functions such as diagnosis [25], and their synthesis into a
fault-tolerant architecture based on active (state-machine) replication [11, 35].
Formal, and especially mechanically-checked, verification of these algorithms is
still something of a tour de force, however. To have real impact on practice, we
need to reduce the difficulty of formal verification in this domain to a routine and
largely automated process. In order to achieve this, we should study the sources
of difficulty in existing treatments and attempt to reduce or eliminate them. In
particular, we should look for opportunities for systematic treatments: these may
allow aspects common to a range of algorithms to be treated in a uniform way, and
may even allow some of those aspects to be broken out and verified in a generic
manner once and for all.
There is a wide range in the apparent level of difficulty and detail in the verifications
cited above. Some of the differences can be attributed to the ways in which
the problems are formalized or to the different resources of the formal specification
languages and theorem provers employed. For example, Rushby [34] and Bevier
and Young [2] describe mechanically checked formal verifications of the same "Oral
Messages" algorithm [24] for the consensus problem that were performed using different
verification systems. Young [42] argues that differences in the difficulty of
these treatments (that of [34] is generally considered simpler and clearer than that
of [2]) are due to different choices in the way things are formalized. We may assume
that such differences will be reduced or eliminated as experience is gained and the
better choices become more widely known.
More significant than differences due to how things are formalized are differences
due to what is formalized, and the level of detail considered necessary. For exam-
ple, both verifications of the Oral Messages algorithm mentioned above specify
the algorithm as a functional program and the proofs are conventional inductions.
Following this approach, the special case of a two-round algorithm (a variant of the
algorithm known as OM(1)) is specified in [28] in a couple of lines and its verification
is almost completely automatic. In contrast, the treatment of OM(1) in [23]
is long and detailed and quite complicated. The reason for its length and complexity
is that this treatment explicitly considers the distributed, message passing
character of the intended implementation, and calculates tight real-time bounds
on the timeouts employed. All these details are abstracted away in the treatments
using functional programs-but this does not mean these verifications are inferior
to the more detailed analyses: on the contrary, I would argue that they capture
the essence of the algorithms concerned (i.e., they explain why the algorithm is
fault tolerant) and that message-passing and real-time bounds are implementation
details that ought to be handled separately. In fact, most of the papers that introduce
the algorithms concerned, and the standard textbook [29], use a similarly
abstract and time-free treatment. On the other hand, it is undeniably important
also to verify a specification that is reasonably close to the intended implementa-
tion, and to establish that the correct timeouts are used, and that the concrete
fault modes match those assumed in the more abstract treatment.
The natural resolution for these competing claims for abstractness and concreteness
is a hierarchical approach in which the essence of the algorithm is verified in
an abstract formulation, and a more realistic formulation is then shown to be a
refinement, in some suitable sense, of the abstract formulation. If things work
out well, the refinement argument should be a routine calculation of timeouts and
other concrete details. The purpose of this paper is to present a framework for such
a hierarchical treatment and to show that, for the important case of time-triggered
implementations of round-based algorithms, most of the details of the refinement
to a concrete formulation can be worked out once and for all.
Systematic Formal Verification for Time-Triggered Algorithms 5
Round-Based Algorithms
In her textbook [29], Nancy Lynch identifies algorithms for the synchronous
system model with those that execute in a series of "rounds." Rounds have two
phases: in the first, each processor 1 sends a message to some or all of the other
processors (different messages may be sent to different processors; the messages
will depend on the current state of the sending processor); in the second phase,
each processor changes its state in a manner that depends on its current state
and the collection of messages it received in the first phase. There is no notion of
real-time in this model: messages are transferred "instantaneously" from senders
to recipients between the two phases. The processors operate in lockstep: all of
them perform the two phases of the current round, then move on to the first phase
of the next round, and so on.
Several of the algorithms of interest here were explicitly formulated in terms of
rounds when first presented, and others can easily be recast into this form. For
example, the Oral Messages algorithm for consensus, OM(1), requires two rounds
as follows.
Algorithm OM(1)
Round 0:
Communication Phase: A distinguished processor called the transmitter
sends a value to all the other processors, which are called receivers; the
receivers send no messages.
Computation Phase: Each receiver stores the value received from the
transmitter in its state.
Round 1:
Communication Phase: Each receiver sends the value it received from the
transmitter to all the other receivers; the transmitter sends no message.
Computation Phase: Each receiver sets the "decision" component of its
state to the majority value among those received from the other receivers
and that (stored in its state) received from the transmitter.
In the presence of one or fewer arbitrary faults, OM(1) ensures that all nonfaulty
receivers decide on the same value and, if the transmitter is nonfaulty, that value
is the one sent by the transmitter.
There are two different ways to implement round-based algorithms. In the time-triggered
approach, the implementation is very close to the model: the processors
are closely synchronized (e.g., to within a couple of bit-times in the case of
I refer to the participants as processors to stress that they are assumed to fail independently;
the agents that perform these actions will actually be processes.
SAFEbus) and all run a common, deterministic schedule that will cause them to
execute specific algorithms at specific times (according to their local clocks). The
sequencing of phases and rounds is similarly driven by the local clocks, and communication
bandwidth is also allocated as dedicated, fixed, time slots. The first
(communication) phase in each round must be sufficiently long that all nonfaulty
processors will be able to exchange messages successfully; consequently, no explicit
timeouts are needed: a message that has not arrived by the time the second
(computation) phase of a round begins is implicitly timed out.
Whereas the allocation of resources is statically determined in the time-triggered
approach, in the other, event-triggered, approach, resources are scheduled dynamically
and processors respond to events as they occur. In this implementation
style, the initiation of a protocol may be triggered by a local clock, but subsequent
phases and rounds are driven by the arrival of messages. In Lamport and Merz'
treatment of OM(1), for example, a receiver that has received a message from the
transmitter may forward it immediately to the other receivers without waiting for
the clock to indicate that the next round has started (in other words, the pacing
of phases and rounds is determined locally by the availability of messages). Unlike
the time-triggered approach, messages may have to be explicitly timed out in
the event-triggered approach. For example, in Lamport and Merz' treatment of
OM(1), a receiver will not wait for relayed messages from other receivers beyond
past the start of the algorithm (where ffi is the maximum communication
delay and ffl the maximum time that it can take a receiver to decide to relay a
message).
Some algorithms were first introduced using an event-triggered formulation (for
example, Cristian's atomic broadcast and group membership algorithms [7, 9]),
but it is possible to reconstruct explicitly round-based equivalents for them, and
then transform them to time-triggered implementations (Kopetz' time-triggered
algorithms [19] for the same problems do this to some extent). Event-triggered
systems are generally easier to construct than time-triggered ones (which require
a big planning and scheduling effort upfront) and achieve better CPU utilization
under light load. On the other hand, Kopetz [20,21] argues persuasively that time-triggered
systems are more predictable (and hence easier to verify), easier to test,
make better use of broadcast communications bandwidth (since no addresses need
be communicated-these are implicit in the time at which a message is sent), can
operate closer to capacity, and are generally to be preferred for truly critical appli-
cations. The previously mentioned SAFEbus for the Boeing 777, the Shinkansen
train control system, and the TTP protocol for automobiles are all time-triggered.
Our goal is a systematic method for transforming round-based protocols from
very abstract functional programs, whose properties are comparatively easy to
formally and mechanically verify, down to time-triggered implementations with
appropriate timing constraints and consideration for realistic fault modes. The
transformation is accomplished in two steps: first from a functional program to
an (untimed) synchronous system, then to a time-triggered implementation. The
first step is systematic but must be undertaken separately for each algorithm (see
Systematic Formal Verification for Time-Triggered Algorithms 7
Section 4); the other is generic and deals with a large class of algorithms and fault
assumptions in a single verification. This generic treatment of the second step is
described in the following section.
Round-Based Algorithms Implemented as Time-Triggered Systems
The issues in transforming an untimed round-based algorithm to a time-triggered
implementation are basically to ensure that the timing and duration of events in
the communication phase are such that messages between nonfaulty processors
always arrive in the communication phase of the same round, and fault modes
are interpreted appropriately. To verify the transformation, we introduce formal
models for untimed synchronous systems and for time-triggered systems, and then
establish a simulation relation between them. This treatment has been formalized
and mechanically checked using the PVS verification system-see Section 3.4.
3.1 Synchronous Systems
For the untimed case, we use Nancy Lynch's formal model for synchronous
systems [29, Chapter 2], with some slight adjustments to the notation that make
it easier to match up with the mechanically verified treatment.
Untimed Synchronous Systems.
We assume a set mess of messages that includes a distinguished value null, and
a set proc of processors. Processors are partially connected by directed channels;
each channel can be thought of a buffer that can hold a single message. Associated
with each processor p are the following sets and functions.
ffl A set of processors out-nbrs p
to which p is connected by outgoing channels.
ffl A set of processors in-nbrs p
to which p is connected by incoming channels;
the function inputs p
mess gives the message contained in each
of those channels.
ffl A set states p
of states with a nonempty subset init p
of initial states. It is
convenient to assume that there is a component in the state that counts
rounds; this counter is zero in initial states.
ffl A function msg p
states p
\Theta out-nbrs p
mess that determines the message
to be placed in each outgoing channel in a way that depends on the current
state.
ffl A function trans p
states p
\Theta inputs p
states p
that determines the next
state, in a way that depends on the current state and the messages received
in the incoming channels.
The system starts with each processor in an initial state. All processors p then
repeatedly perform the following two actions in lockstep.
Communication Phase: apply the message generation function msg p
to the current
state to determine the messages to be placed in each outgoing channel.
(The message value null is used to indicate "no message.")
Computation Phase: apply the state transition function trans p
to the current
state and the message held in each incoming channel to yield the next state
(with the round counter incremented).A particular algorithm is specified by supplying interpretations to the various sets
and functions identified above.
Faults. Distributed algorithms are usually required to operate in the presence of
faults: the specific kinds and numbers of faults that may arise constitute the fault
hypothesis. Usually, processor faults are distinguished from communication faults;
the former can be modeled by perturbations to the transition functions trans p
and the latter by allowing the messages received along a channel to be changed
from those sent. Following [29, page 20], an execution of the system is then an
infinite sequence of triples
is the global state at the start of round r, M r
is the collection of messages
placed in the communication channels, and N r
is the (possibly different) collection
of messages received.
Because our goal is to show that a time-triggered implementation achieves the
same behavior as the untimed synchronous system that serves as its specification,
we will need some way to ensure that faults match up across the two systems. For
this reason, I prefer to model processor and communications faults by perturbations
to the trans p
and msg p
respectively (rather than allowing messages
received to differ from those sent). In particular, I assume that the current round
number is recorded as part of the state and that if processor p is faulty in round
r, with current state s and the values of its input channels represented by the
array i, then trans p
(s; i) may yield a value other than that intended; similarly,
if the channel from p to q is faulty, then the value msg p
(s)(q) may be different
than intended (and may be null). Exactly how these values may differ from those
intended depends on the fault assumption. For example, a crash fault in round r
results in trans p
null for all i, q, and states s whose
round component is r or greater. Notice that although trans p
and msg p
may no
longer be the intended functions, they are still functions; in fact, there is no need
to suppose that the trans p
and msg p
were changed when the fault arrived in round
Systematic Formal Verification for Time-Triggered Algorithms 9
r: since the round counter is part of the state, we can just assume these functions
behave differently than intended when applied to states having round counters
equal or greater than r.
The benefit of this treatment is that, since trans p
and msg p
are uninterpreted,
they can represent any algorithm and any fault behavior; if we can show that
a time-triggered system supplied with arbitrary trans p
and msg p
functions has
the same behavior as the untimed synchronous system supplied with the same
functions, then this demonstration encompasses behavior in the presence of faults
as well as the fault-free case. Furthermore, since we no longer need to hypothesize
that faults can cause differences between those messages sent and those received
(we instead assume the fault is in msg p
and the "different" messages were actually
sent), executions can be simplified from sequences of triples to simple sequences of
states
is the global state at the start of round r. Consequently, to demonstrate
that a time-triggered system implements the behavior specified by an untimed
synchronous system, we simply need to establish that both systems have the same
execution sequences; by mathematical induction, this will reduce to showing that
the global states of the two systems are the same at the start of each round r.
3.2 Time-Triggered Systems
For the time-triggered system, we elaborate the model of the previous section
as follows.
Each processor is supplied with a clock that provides a reasonably accurate
approximation to "real" time. When speaking of clocks, it is usual to distinguish
two notions of time: clocktime, denoted C is the local notion of time supplied by
each processor's clock, while realtime, denoted R is an abstract global quantity. It
is also usual to denote clocktime quantities by upper case Roman or Greek letters,
and realtime quantities by lower case letters.
Formally, processor p's clock is a function C p
C. The intended interpretation
is that C p
(t) is the value of p's clock at realtime t. 2 The clocks of nonfaulty
processors are assumed to be well-behaved in the sense of satisfying the following
assumptions.
Assumption 1 Monotonicity. Nonfaulty clocks are monotonic increasing functions

Satisfying this assumption requires some care in implementation, because clock
synchronization algorithms can make adjustments to clocks that cause them to
2 In the terminology of [22], these are actually "inverse" clocks.
jump backwards. Lamport and Melliar-Smith describe some solutions [22], and
a particularly clever and economical technique for one particular algorithm is introduced
by Torres-Pomales [40] and formally verified by Miner and Johnson [30].
Schmuck and Cristian [38] examine the general case and show that monotonicity
can be achieved with no loss of precision.
Assumption 2 Clock Drift Rate. Nonfaulty clocks drift from realtime at a rate
bounded by a small positive quantity ae (typically
Assumption 3 Clock Synchronization. The clocks of nonfaulty processors are
synchronized within some small clocktime bound \Sigma:
(t)j  \Sigma:
Systems.
The feature that characterizes a time-triggered system is that all activity is
driven by a global schedule: a processor performs an action when the time on its
local clock matches that for which the action is scheduled. In our formal model,
the schedule is a function sched is the clocktime at
which round r should begin. The duration of the r'th round is given by
In addition, there are fixed global clocktime constants D and P that give the
offsets into each round when messages are sent, and when the computation phase
begins, respectively. Obviously, we need the following constraint.
Constraint
Notice that the duration of the communication phase is fixed (by P ); it is only the
duration of the computation phase that can differ from one round to another. 3
The states, messages, and channels of a time-triggered system are the same as
those for the corresponding untimed synchronous system, as are the transition
and message functions. In addition, processors have a one-place buffer for each
incoming message channel.
The time-triggered system operates as follows. Initially each processor is in an
initial state, with its round counter zero and its clock synchronized with the others
and initialized so that C p
is the current realtime. All
processors p then repeatedly perform the following two actions.
3 In fact, there is no difficulty in generalizing the treatment to allow the time at which messages
are sent, and the duration of the communication phase, to vary from round to round. That is,
the fixed clocktime constants D and P can be systematically replaced by functions D(r) and
P (r), respectively. This generalization was developed during the mechanized verification; see
Section 3.4.
Systematic Formal Verification for Time-Triggered Algorithms 11
Communication Phase: This begins when the local clock reads sched (r), where
r is the current value of the round counter. Apply the message generation
function msg p
to the current state to determine the messages to be sent on
each outgoing channel. The messages are placed in the channels at local clock
time sched(r)+D. Incoming messages that arrive during the communication
phase (i.e., no later than sched(r) are moved to the corresponding input
buffer where they remain stable through the computation phase. These
buffers are initialized to null at the beginning of each communication phase
and their value is unspecified if more than one message arrives on their associated
communications channel in a given communication phase.
Computation Phase: This begins at local clock time Apply the
state transition function trans p
to the current state and the messages held in
the input buffers to yield the next state. The computation will be complete
at some local clock time earlier than sched(r 1). Increment the round
counter, and wait for the start of the next round.Message transmission in the communication phase is explained as follows. We
use sent(p; q; m; t) to indicate that processor p sent message m to processor q (a
member of out-nbrs(p)) at real time t (which must satisfy C p
for some round r). We use recv(q; to indicate that processor q received
message m from processor p (a member of in-nbrs(q)) at real time t (which must
satisfy the constraint sched(r)  C q
round r). These
two events are related as follows.
Assumption 4 Maximum Delay. When p and q are nonfaulty processors,
sent (p; q; m; t) oe recv(q; d)
for some 0  d  ffi.
In addition, we require no spontaneous generation of messages (i.e., recv(q;
only if there is a corresponding sent (p; q; m; t 0 )).
Provided there is exactly one recv(q; event for each p in the communication
phase for round r on processor q (as there will be if p is nonfaulty), that
message m is moved into the input buffer associated with p on processor q before
the start of the computation phase for that round and remains there throughout
the phase.
Because the clocks are not perfectly synchronized, it is possible for a message sent
by a processor with a fast clock to arrive while its recipient is still on the previous
round. It is for this reason that we do not send messages until D clocktime units
into the start of the round. In general, we need to ensure that a message from
a processor in round r cannot arrive at its destination before that processor has
started round r, nor after it has finished the communication phase for round r. We
must establish constraints on parameters to ensure these conditions are satisfied.
Now processor p sends its message to processor q, say, at realtime t where C p
and, by the maximum delay assumption, the message will arrive at
We need to be sure that
By clock synchronization, we have jC q
(t)j  \Sigma; substituting C p
sched(r) +D we obtain
By the monotonic clocks assumption, this gives
d)
and so the first inequality in (1) can be ensured by
Constraint 2 D  \Sigma.
The clock synchronization calculation (2) above also gives
and the clock drift rate assumption gives
from which it follows that
Thus, the second inequality in (1) can be ensured by
Constraint
Faults. We will prove that a time-triggered system satisfying the various assumptions
and constraints identified above achieves the same behavior as an untimed
synchronous system supplied with the same trans p
and msg p
functions. I explained
earlier that faults are assumed to be modeled in the trans p
and msg p
by using the same functions in both the untimed and time-triggered systems, we
ensure that the latter inherits the same fault behavior and any fault-tolerance
properties of the former. Thus, if we have an algorithm that has been shown, in its
untimed formulation, to achieve some fault-tolerance properties (e.g., "this algorithm
resists a single Byzantine fault or two crash faults"), then we may conclude
that the implementation has the same properties.
Systematic Formal Verification for Time-Triggered Algorithms 13
This simple view is somewhat compromised, however, because the time-triggered
system contains a mechanism-time triggering-that is not present in the untimed
system. This mechanism admits faults (notably, loss of clock synchronization) that
do not arise in the untimed system. An implementation must ensure that such
faults are either masked, or are transformed in such a way that their manifestations
are accurately modeled by perturbations in the trans p
and msg p
functions.
In general, it is desirable to transform low-level faults (i.e., those outside the
model considered here) into the simplest (most easily tolerated) fault class for the
algorithm concerned. If no low-level mechanism for dealing with loss of clock synchronization
is present, then synchronization faults may manifest themselves as
arbitrary, Byzantine faults to the abstract algorithm. For example, if one pro-
cessor's clock drifts to such an extent that it is in the wrong round, then it will
execute the transition and message functions appropriate to that round and will
supply systematically incorrect messages to the other processors. This could easily
appear as Byzantine behavior at the level of the untimed synchronous algorithm.
For this reason, it is desirable to include the round number in messages, so that
those from the wrong round can be rejected (thereby reducing the fault manifestation
to fail-silence). TTP goes further and includes all critical state information
(operating mode, time, and group membership) in its messages as part of the CRC
calculation [21].
Less drastic clock skews may leave a processor in the right round, but sending
messages at the wrong time, so that they arrive during the computation phases of
the other (correct) processors. It is partly to counter this fault mode that the time-triggered
model used here explicitly moves messages from their input channels to an
input buffer during the communication phase: this shields the receiving processor
from any changes in channel contents during the computation phase.
If the physical implementation of the time triggered system multiplexes its communications
channels onto shared buses, then it is necessary to control the "bab-
bling idiot" fault mode where a faulty processor disrupts the communications of
other processors by speaking out of turn. In practice, this is controlled by a Bus
Interface Unit (BIU) that only grants access to the bus at appropriate times. For
example, in SAFEbus, processors are paired, with each member of a pair controlling
the other's BIU; in TTP, the BIU has independent knowledge of the schedule.
In both cases, babbling can occur only if there are undetected double failures.
3.3 Verification
We now need to show that a time-triggered system achieves the same behavior
as its corresponding untimed synchronous system. We do this in the traditional
way by establishing a simulation relationship between the states of an execution
of the time-triggered system and those of the corresponding untimed execution.
It is usually necessary to invent an "abstraction function" to relate the states of
an implementation to those of its specification; here, however, the states of the
two systems are the same, and the only difficult point is to select the moments in
time at which states of the time-triggered system should correspond to those of
the untimed system.
The untimed system makes progress in discrete global steps: all component
processors perform their communication and computation phases in lockstep, so
it is possible to speak of the complete system being in a round r. The processors
of the time-triggered system, however, progress separately at a rate governed by
their internal clocks, which are imperfectly synchronized, so that one processor
may still be on round r while another has moved on to round r + 1. We need to
establish some consistent "cut" through the time-triggered system that provides a
global state in which all processors are at the same point in the same round. In
some treatments of distributed systems, it is not necessary for the global cut to
correspond to a snapshot of the system at a particular realtime instant: the cut may
be an abstract construction that has no direct realization. In our case, however,
it is natural to assume that the time-triggered system is used in some control
application and that outputs of the individual processors (i.e., some functions
of their states) are used to provide redundant control signals in real time-for
example, a typical application will be one in which the outputs of the processors
are subjected to majority voting, or separately drive some actuator in a "force-
summing" configuration. 4 Consequently, we do want to identify the cut through
the system with its global state at a specific real time instant.
In particular, we need some realtime instant gs(r) that corresponds to the
"global start" of the r'th round. We want this instant to be one in which all
nonfaulty processors have started the r'th round, but have not yet started its
computation phase (when they will change their states).
We can achieve this by defining the global start time gs(r) for round r to be the
realtime when the processor with the slowest clock begins round r. That is, gs(r)
satisfies the following constraints:
and
sched (r) (4)
(intuitively, p is the processor with the slowest clock).
Since the processors are not perfectly synchronized, we need to be sure that they
cannot drift so far apart that some processor q has already reached its computation
phase-or is even on the next round-at gs(r). Thus, we need
By (3) we have C q
plus the clock
synchronization assumption then gives X  \Sigma. Now processor q will still be on
4 For example, the outputs of different processors may energize separate coils of a single
solenoid, or multiple hydraulic pistons may be linked to a single shaft (see, e.g., [12, Figure
3.2-2]).
Systematic Formal Verification for Time-Triggered Algorithms 15
round r and in its communication phase provided this is ensured by
the inequality just derived when taken together with Constraint 3.
We now wish to establish that the global state of a time-triggered system at time
gs(r) will be the same as that of the corresponding untimed synchronous system
at the start of its r'th round. We denote the global state of the untimed system at
the start of the r'th round by gu(r) (for global untimed ). Global states are simply
arrays of the states of the individual processors, so that the state of processor p
at this point is gu(r)(p). Similarly, the global state of the time-triggered system
at time gs(r) is denoted gt(r) (for global timed ), and the state of its processor p is
gt(r)(p). We can now state and prove the desired result.
Theorem 1 Given the same initial states, the global states of the untimed and
time-triggered systems are the same at the beginning of each round:
Proof: The proof is by induction.
Base case. This is the case systems are then in their initial states
which, by hypothesis, are the same.
Inductive step. We assume the result for r and prove it for r + 1. For the
untimed case, the message inputs q
(p) from processor p received by q in the r'th
round is msg p
(gu(r)(p))(q). 5
By the inductive hypothesis, the global state of processor p in the time-triggered
system at time gs(r) is gu(r)(p) also. Furthermore, processor p is in its communication
phase (ensured by (5)) and has not changed its state since starting the
round. Thus, at local clocktime sched(r) +D, it sends msg p
(gu(r)(p))(q) to q. By
(1), this is received by q while in the communication phase of round r, and transferred
to its input buffer inputs q
(p). Thus, the corresponding processors of the
untimed and time-triggered systems have the same state and input components
when they begin the computation phase of round r. The same state transition
functions trans p
are then applied by the corresponding processors of the two systems
to yield the same values for the corresponding elements of gu(r
completing the inductive proof.5 For the benefit of those not used to reading Curried higher-order function applications, this
is decoded as follows: gu(r)(p) is p's state in round
applied to that
state gives msg p
(gu(r)(p)), which is an array of the messages sent to its outgoing channels; q's
component of that array is msg p
(gu(r)(p))(q).
3.4 Mechanized Verification
The treatment of synchronous and time-triggered systems in Sections 3.1 and 3.2
has been formally specified in the language of the PVS verification system [32], and
the verification of Section 3.3 has been mechanically checked using PVS's theorem
prover. The PVS language is a higher-order logic with subtyping, and formalization
of the semiformal treatment in Sections 3.1 and 3.2 was quite straightforward. The
PVS theorem prover includes decision procedures for integer and real linear arithmetic
and mechanized checking of the calculations in Section 3.3, and the proof
of the Theorem, were also quite straightforward. The complete formalization and
mechanical verification took less than a day, and no errors were discovered. The formal
specification and verification are described in the Appendix; the specification
files themselves are available at URL http://www.csl.sri.com/dcca97.html.
While it is reassuring to know that the semiformal development withstands
mechanical scrutiny, we have argued previously (for example, [32,36]) that mechanized
formal verification provides several benefits in addition to the "certification"
of proofs. In particular, mechanization supports reliable and inexpensive exploration
of alternative designs, assumptions, and constraints. In this case, I wondered
whether the requirement that messages be sent at the fixed offset D clocktime units
into each round, and that the computation phase begin at the fixed offset P , might
not be unduly restrictive. It was the work of a few minutes to generalize the formal
specification to allow these offsets to become functions of the round, and to adjust
the mechanized proofs. I contend that corresponding revisions to the semiformal
development in Sections 3.2 and 3.3 would take longer than this, and that it would
be difficult to summon the fortitude to scrutinize the revised proofs with the same
care as the originals.
Round-Based Algorithms as Functional Programs
The Theorem of Section 3.3 ensures that synchronous algorithms are correctly
implemented by time-triggered implementations that satisfy the various assump-
tions, constraints, and constructions introduced in the previous section. The next
(though logically preceding) step is to ask how one might verify properties of a
particular algorithm expressed as an untimed synchronous system.
Although simpler than its time-triggered implementation, the specification of
an algorithm as a synchronous system is not especially convenient for formal (and
particularly mechanized) verification because it requires reasoning about attributes
of imperative programs: explicit state and control. It is generally easier to verify
rather than imperative, programs because these represent state and
control in an applicative manner that can be expressed directly in conventional
logic.
There is a fairly systematic transformation between synchronous systems and
functional programs that can ease the verification task by allowing it to be performed
on a functional program. I illustrate the idea (which comes from Bevier
Systematic Formal Verification for Time-Triggered Algorithms 17
and Young [2]) using the OM(1) algorithm from Section 2. Because that algorithm
has already been introduced as a synchronous system, I will illustrate its transformation
to a functional program; once the technique becomes familiar, it is easy to
perform the transformation in the other direction.
We begin by introducing a function send(r; v; p; q) to represent the sending of a
message with value v from processor p to processor q in round r. The value of the
function is the message received by q. If p and q are nonfaulty, then this value is
v:
otherwise it depends on the fault modes considered (in the Byzantine case it is left
entirely unconstrained, as here).
If T represents the transmitter, v its value, and q an arbitrary receiver, then the
communication phase of the first round of OM(1) is represented by
The computation phase of this round simply moves the messages received into the
states of the processors concerned, and can be ignored in the functional treatment
(though see Footnote 6).
In the communication phase of the second round, each processor q sends the
value received in the first round (i.e., send(0; v; T; q)) on to the other receivers. If
p is one such receiver, then this is described by the functional composition
In the computation phase for the second round, processor p gathers all the messages
received in the communication phase and subjects them to majority voting. 6 Now
(6) represents the value p receives from q, so we need to gather together in some
way the values in the messages p receives from all the other receivers q, and use that
combination as an argument to the majority vote function. How this "gathering
together" is represented will depend on the resources of the specification language
and logic concerned: in the treatment using the Boyer-Moore logic, for example,
it is represented by a list of values [2]. In a higher-order logic such as PVS [32],
however, it can be represented by a function, specified as a -abstraction:
(i.e., a function that, when applied to q, returns the value that p received from q).
Majority voting is represented by a function maj that takes two arguments: the
"participants" in the vote, and a function over those participants that returns the
6 In the formulation of the algorithm as a synchronous system, p votes on the messages from
the other receivers, and the message that it received directly from the transmitter, which it has
saved in its state. In the functional treatment, q includes itself among the recipients of the
message that it sends in the communication phase of the second round, and so the vote is simply
over messages received in that round.
value associated with each of them. The function maj returns the majority value
if one exists; otherwise some functionally determined value. (This behavior can
either be specified axiomatically, or defined constructively using an algorithm such
as Boyer and Moore's linear time MJRTY [4].) Thus, p's decision in the computation
phase of the second round is represented by
where rcvrs is the set of all receiver processors. We can use this formula as the
definition for a higher-order function OM1(T; v) whose value is a function that
gives the decision reached by each receiver p when the (possibly faulty) transmitter
T sends the value
The properties required of this algorithm are the following, provided the number
of receivers is three or more, and at most one processor is faulty:
Definition (7) and the requirements for Agreement and Validity stated above are
acceptable as specifications to PVS almost as given (PVS requires we be a little
more explicit about the types and quantification involved). Using a constructive
definition for maj, PVS can prove Agreement and Validity for a specific number
of processors (e.g., completely automatically. For the general case of n  4
processors, PVS is able to prove Agreement with only a single user-supplied proof
directive, while Validity requires half a dozen (the only one requiring "insight" is
a case-split on whether the transmitter is faulty).
Not all synchronous systems can be so easily transformed into a recursive func-
tion, nor can their properties always be formally verified so easily. Nonetheless,
I believe the approach has promise for many algorithms of practical interest. A
similar method has been advocated by Florin, G'omez, and Lavall'ee [14].
5 Conclusion
Many round-based fault-tolerant algorithms can be formulated as synchronous
systems. I have shown that synchronous systems can be implemented as time-triggered
systems and have proved that, provided care is taken with fault modes,
the correctness and fault-tolerance properties of an algorithm expressed as a synchronous
system are inherited by its time-triggered implementation. The proof
identifies necessary timing constraints and is independent of the particular algorithm
concerned; it provides a more general and abstract treatment of the analysis
Systematic Formal Verification for Time-Triggered Algorithms 19
performed for a particular system by Di Vito and Butler [5]. The relative simplicity
of the proof supports the argument that time-triggered systems allow for
straightforward analysis and should be preferred in critical applications for that
reason [20].
I have also shown, by example, how a round-based algorithm formulated as a
synchronous system can be transformed into a functional "program" in a specification
logic, where its properties can be verified more easily, and more mechanically.
Systematic transformations of fault-tolerant algorithms from functional programs
to synchronous systems to time-triggered implementations provides a
methodology that can significantly ease the specification and assurance of critical
fault-tolerant systems. In current work, we are applying the methodology to
some of the algorithms of TTP [21].

Acknowledgments

Discussions with N. Shankar and advice from Joseph Sifakis were instrumental
in the development of this work. Comments by the anonymous referees improved
the presentation.



--R

ARINC Specification 659: Backplane Data Bus.
The design and proof of correctness of a fault-tolerant circuit


On the impossibility of group membership.
Reaching agreement on processor-group membership in synchronous distributed systems
Understanding fault-tolerant distributed systems
Atomic broadcast: From simple message diffusion to Byzantine agreement.

Di Vito and
The General Dynamics Case Study on the F16 Fly-by-Wire Flight Control System
Impossibility of distributed consensus with one faulty process.
Systematic building of a distributed recursive algorithm.
Group membership protocol: Specification and verification.
The concepts and technologies of dependable and real-time computer systems for Shinkansen train control
SAFEbus TM
Fault Tolerant Computing Symposium 25: Highlights from 25 Years

Should responsive systems be event-triggered or time-triggered? IEICE Transactions on Information and Systems

Synchronizing clocks in the presence of faults.
Specifying and verifying fault-tolerant systems
The Byzantine Generals problem.
Formally verified algorithms for diagnosis of manifest
Formal verification of an algorithm for interactive consistency under a hybrid fault model.
A formally verified algorithm for interactive consistency under a hybrid fault model.
Formal verification of an interactive consistency algorithm for the Draper FTP architecture under a hybrid fault model.
Distributed Algorithms.
Verification of an optimized fault-tolerant clock synchronization circuit: A case study exploring the boundary between formal reasoning systems
Integrated modular avionics for next-generation commercial airplanes
Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS
Reaching agreement in the presence of faults.
Formal verification of an Oral Messages algorithm for interactive consistency.
A fault-masking and transient-recovery model for digital flight-control systems
A formally verified algorithm for clock synchronization under a hybrid fault model.
A less elementary tutorial for the PVS specification and verification system.
Continuous clock amortization need not affect the precision of a clock synchronization algorithm.
Boeing's seventh wonder.
An optimized implementation of a fault-tolerant clock synchronization circuit
Formal Techniques in Real-Time and Fault-Tolerant Systems
Comparing verification systems: Interactive Consistency in ACL2.
Formal specification and compositional verification of an atomic broadcast protocol.
--TR

--CTR
Clara Benac Earle , Lars-ke Fredlund , John Derrick, Verifying fault-tolerant Erlang programs, Proceedings of the 2005 ACM SIGPLAN workshop on Erlang, September 26-28, 2005, Tallinn, Estonia
Christoph Kreitz, Building reliable, high-performance networks with the Nuprl proof development system, Journal of Functional Programming, v.14 n.1, p.21-68, January 2004
Faith Fich , Eric Ruppert, Hundreds of impossibility results for distributed computing, Distributed Computing, v.16 n.2-3, p.121-163, September
formal verification;formal methods;time-triggered algorithms;synchronous systems;PVS