An inheritance-based technique for building simulation proofs incrementally.
This paper presents a technique for incrementally constructing safety specifications, abstract algorithm descriptions, and simulation proofs showing that algorithms meet their specifications.The technique for building specifications (and algorithms) allows a child specification (or algorithm) to inherit from its parent by two forms of incremental modification: (a) interface extension, where new forms of interaction are added to the parent's interface, and (b) specialization (subtyping), where new data, restrictions, and effects are added to the parent's behavior description. The combination of interface extension and specialization constitutes a powerful and expressive incremental modification mechanism for describing changes that do not override the behavior of the parent, although it may introduce new behavior.Consider the case when incremental modification is applied to both a parent specification S and a parent algorithm A. A proof that the child algorithm A implements the child specification S can be built incrementally upon simulation proof that algorithm A implements specification S. The new work required involves reasoning about the modifications, but does not require repetition of the reasoning in the original simulation proof.The paper presents the technique mathematically, in terms of automata. The technique has already been used to model and validate a full-fledged group communication system (see [26]); the methodology and results of that experiment are summarized in this paper.
INTRODUCTION
Formal modeling and validation of software systems is
a major challenge, because of their size and complex-
ity. Among the factors that could increase widespread
usage of formal methods is improved cost-effectiveness
and scalability (cf. [20, 22]). Current software engineering
practice addresses problems of building complex systems
by the use of incremental development techniques
based on an object-oriented approach. We believe that
successful efforts in system modeling and validation will
also require incremental techniques, which will enable
reuse of models and proofs.
In this paper we provide a framework for reuse of
proofs analogous and complementary to the reuse provided
by object-oriented software engineering method-
ologies. Specifically, we present a technique for incrementally
constructing safety specifications, abstract algorithm
descriptions, and simulation proofs that algorithms
specifications. Simulation proofs are
one of the most important techniques for proving properties
of complex systems; such proofs exhibit a simulation
relation (refinement mapping, abstraction func-
tion) between a formal description of a system and its
specification [13, 24, 29].
The technique presented in this paper has evolved with
our experience in the context of a large-scale modeling
and validation project: we have successfully used
this technique for modeling and validating a complex
group communication system [26] that is implemented
in C++, and that interacts with two other services developed
by different teams. The group communication
system acts as middleware in providing tools for building
distributed applications. In order to be useful for
a variety of applications, the group communication system
provides services with diverse semantics that bear
many similarities, yet differ in subtle ways. We have
modeled the diverse services of the system and validated
the algorithms implementing each of these ser-
vices. Reuse of models and proofs was essential in order
to make this task feasible. For example, it has allowed
us to avoid repeating the five-page long correctness
proof of the algorithm that provides the most basic
semantics when proving the correctness of algorithms
that provide the more sophisticated semantics. The correctness
proof of the most sophisticated algorithm, by
comparison, was only two and a half pages long. (We
describe our experience in this project as well as the
methodology that evolved from it in Section 6.)
Our approach to the reuse of specifications and algorithms
through inheritance uses incremental modification
to derive a new component (specification or algo-
rithm), called child , from an existing component called
parent . Specifically, we present two constructions for
modifying existing components:
1. We allow the child to specialize the parent by
reusing its state in a read-only fashion, by adding
new state components (read/write), and by constraining
the set of behaviors of the parent. This
corresponds to the subtyping view of inheritance [8].
We will show that any observable behavior of the
child is subsumed (cf. [1]) by the possible behaviors
of the parent, making our specialization analogous
to the substitution inheritance [8]. In particular,
the child can be used anywhere the parent can be
used. (Specialization is the subject of Section 3.)
2. A child can also be derived from a parent by means
of interface (signature) extension. In this case the
state of the parent is unchanged, but the child may
include new observable actions not found in the
parent and new parameters to actions that exist
at the parent. When such new actions and parameters
are hidden, then any behavior of the child is
exactly as some behavior of the parent. (Interface
extension is presented in Section 5.)
When interface extension is combined with specializa-
tion, this corresponds to the subclassing for extension
form of inheritance [8] which provides a powerful mechanism
for incrementally constructing specifications and
algorithms. Consider the following example. The parent
defines an unordered messaging service using the
send and recv primitives. To produce a totally ordered
messaging service we specialize the parent in such a way
that recv is only possible when the current message is
totally ordered. Next we introduce the safe primitive,
which informs the sender that its message was deliv-
ered. First we extend the service interface to include
safe primitives and then we specialize to enable safe actions
just in case the message was actually delivered.
The specialization and extension constructs can be applied
at both the specification level and the algorithm
level in a way that preserves the relationship between
the specification and the algorithm. The main technical
challenge addressed in this paper (in Section 4) is the
provision of a formal framework for the reuse of simulation
proofs especially for the specialization construct.
Consider the example in Figure 1: Let S be a specifica-
tion, and A an abstract algorithm description. Assume
that we have proven that A implements S using a simulation
relation R p
. Assume further that we specialize
the specification S, yielding a new child specification S 0 .
At the same time, we specialize the algorithm A to construct
an algorithm A 0 which supports the additional
semantics required by S 0 .

Figure

Algorithm A simulates specification S with
. Can R p
be reused for building a simulation R c
from
a child A 0 of A to a child S 0 of S?
A
A'
simulation
simulation
Rp
inheritance
inheritance
When proving that A 0 implements S 0 , we would like
to rely on the fact that we have already proven that
A implements S, and to avoid the need to repeat the
same reasoning. We would like to reason only about
the new features introduced by S 0 and A 0 . The proof
extension theorem in Section 4 provides the means for
incrementally building simulation proofs in this manner.
Simulation proofs [13] lend themselves naturally to be
supported by interactive theorem provers. Such proofs
typically break down into many simple cases based on
different actions. These can be checked by hand or with
the help of interactive theorem provers. Our incremental
simulation proofs break down in a similar fashion.
We present our incremental modification constructs in
the context of the I/O automata model [30, 32] (the
basics of the model are reviewed in Section 2). I/O
automata have been widely used in formulating formal
service definitions and abstract implementations, and
for reasoning about them, e.g., [6, 9, 11, 12, 14, 15, 21,
24, 28, 31]). An important feature of the I/O automaton
formalism is its strong support of composition. For
example, Hickey et al. [24] used the compositional approach
for modeling and verification of certain modules
in Ensemble [19], a large-scale, modularly structured,
group communication system. Introducing inheritance
into the I/O automaton model is vital in order to push
the limits of such projects from verification of individual
modules to verification of entire systems, as we have
experienced in our work on such a project [26]. Further-
more, a programming and modeling language based on
I/O automata formalism, IOA [17, 18] has been defined.
We intend to exploit the IOA framework, to develop
IOA-based tools to support the techniques presented in
this paper both for validation and for code generation.
Stata and Guttag [36] have recognized the need for reuse
in a manner similar to that suggested in this paper,
which facilitates reasoning about correctness of a sub-class
given the correctness of the superclass is known.
They suggest a framework for defining programming
guidelines and supplement this framework with informal
rules that may be used to facilitate such reason-
ing. However, they only address informal reasoning and
do not provide the mathematical foundation for formal
proofs. Furthermore, [36] is restricted to the context of
sequential programming and does not encompass reactive
components as we do in this paper.
Many other works, e.g., [1, 6, 10, 23, 25, 33], have formally
dealt with inheritance and its semantics. Our distinguishing
contribution is the provision of a mathematical
framework for incremental construction of simulation
proofs by applying the formal notion of inheritance
at two levels: specification and algorithm.
This section presents background on the I/O automaton
model, based on [30], Ch. 8. In this model, a system
component is described as a state-machine, called an
I/O automaton. The transitions of the automaton are
associated with named actions, classified as input, output
and internal. Input and output actions model the
component's interaction with other components, while
internal actions are externally unobservable.
Formally, an I/O automaton A consists of: an interface
(or signature), sig(A), consisting of input, output and
internal actions; a set of states, states(A); a set of start
states, start(A); and a state-transition relation (a sub-set
of states(A) \Thetasig(A) \Thetastates(A)), trans(A).
An action  is said to be enabled in a state s if the automaton
has a transition of the form (s, , s'); input actions
are enabled in every state. An execution of an automaton
is an alternating sequence of states and actions
that begins with a start state, and successive triples are
allowable transitions. A trace is a subsequence of an
execution consisting solely of the automaton's external
actions. The I/O automaton model defines a composition
operation which specifies how automata interact
via their input and output actions.
I/O automata are conveniently presented using the
precondition-effect style. In this style, typed state variables
with initial values specify the set of states and the
start states. Transitions are grouped by action name,
and are specified using a pre: block with preconditions
on the states in which the action is enabled and an eff:
block which specifies how the pre-state is modified. The
effect is executed atomically to yield the post-state.
Simulation Relations
When reasoning about an automaton, we are only interested
in its externally-observable behavior as reflected in
its traces. A common way to specify the set of traces an
automaton is allowed to generate is using (abstract) I/O
automata that generate the legal sets of traces. An implementation
automaton satisfies a specification if all of
its traces are also traces of the specification automaton.
Simulation relations are a commonly used technique for
proving trace inclusion:
Definition 2.1 Let A and S be two automata with the
same external interface. Then a relation R ' states(A)
\Theta states(S) is a simulation from A to S if it satisfies
the following two conditions:
1. If t is any initial state of A, then there is an initial
state s of S such that s 2 R(t).
2. If t and s 2 R(t) are reachable states of A and
S respectively, and if (t; ; t 0 ) is a step of A, then
there exists an execution fragment of S from s to
having the same trace, and with s
The following theorem emphasizes the significance of
simulation relations. (It is proven in [30], Ch. 8.)
Theorem 2.1 If A and S are two automata with the
same external interface and if R is a simulation from A
to S then traces(A) ' traces(S).
The simulation relation technique is complete: any finite
trace inclusion can be shown by using simulation
relations in conjunction with history and prophecy variables
[2, 35].
Our specialization construct captures the notion of sub-typing
in I/O automata in the sense of trace inclusion;
it allows creating a child automaton which specializes
the parent automaton. The child can read the parent's
state, add new (read/write) state components, and restrict
the parent's transitions. The specialize construct
defined below operates on a parent automaton, and accepts
three additional parameters: a state extension -
the new state components, an initial state extension -
the initial values of the new state components, and a
transition restriction which specifies the child's addition
of new preconditions and effects (modifying new state
components only) to parent transitions. We define the
specialization construct formally below.
Definition 3.1 Let A be an automaton; let N be a set
of states, called a state extension; let N 0
be a non-empty
subset of N, called an initial state extension; let
TR ' (states(A) \Theta N) \Theta sig(A) \Theta N be a relation,
called a transition restriction. For each action , TR
specifies the additional restrictions that a child places
on the states of A and N in which  is enabled and specifies
how the new state components are modified as a
result of a child taking a step involving .
Then specialize(A)(N; defines an automaton A 0
as follows:
Notation 3.2 If A use
the following
to denote its parent component and tj n
to denote its
new component. If ff is an execution sequence of A 0 ,
then ffj p
denotes a sequence obtained by replacing
each state t in ff with tj p
We also extend
this notation to sets of states and to sets of execution
sequences.
We now exemplify the use of the specialization con-
struct. Figure 2 presents a simple algorithm automaton,
write through cache, implementing a sequentially-consistent
register x shared among a set of processes P.
Each process has access to a local cache p
. Register
x is initialized to some default value v 0
. A write p
(v)
request propagates v to both x and cache p
. A response
read p
(v) to a read request returns the value v of p's
local cache p
without ensuring that it is current. Thus,
a process p responds to a read request with a value of x
which is at least as current as the last value previously
seen by p but not necessarily the most up-to-date one.

Figure

3 presents an atomic write-through cache au-
tomaton, atomic write through cache, as a specialization
of write through cache. The specialized
automaton maintains an additional boolean variable
synched p
for each process p in order to restrict
the behavior of the parent so that a response to a read
request returns the latest value of x. The traces of this
automaton are indistinguishable from those of a system
with a single shared register and no cache.
In general, the transition restriction denoted by this
type of precondition-effect code is the union of the following
two sets:
ffl All triples of the form (t; ; tj n
) for which  is
not mentioned in the code for A 0 , i.e., A 0 does not

Figure

Write-through cache automaton.
automaton write through cache
Signature:
Input: write p (v)
read
Output: read p (v)
synch p ()
State:
Transitions:
cache p
INTERNAL synch p ()
eff: cache p
INPUT read req p ()
OUTPUT read p (v)
pre:

Figure

3 Atomic write-through cache automaton.
automaton atomic write through cache
modifies write through cache
State Extension:
initially true
Transition Restriction:
eff: synched q
INTERNAL synch p ()
eff: synched p
true
OUTPUT read p (v)
pre: synched p
true
restrict transitions involving . The read req p
ac-
tion of Figure 2 is an example of such a . Note
that the new state component, tj n
, is not changed.
) in which state t satisfies new
preconditions on  placed by A 0 and in which state
is the result of applying 's new effects to t.
Theorem 3.1 below says that every trace of the specialized
automaton is a trace of the parent automaton.
In Section 4, we demonstrate how proving correctness
of automata presented using the specialization operator
can be done as incremental steps on top of the correctness
proofs of their parents.
Theorem 3.1 If A 0 is a child of an automaton A, then:
1.
execs(A).
2.
Proof 3.1:
1. Straightforward induction on the length of the execution
sequence. Basis: If t 2
by the definition of start(A 0 ).
Inductive Step: If (t; ; t 0 ) is a step of A 0 , then
) is a step of A, by the definition of
2. Follows from Part 1 and the fact that
sig(A). Alternatively, notice that trace inclusion
is implied by Theorem 2.1 and the fact that the
function that maps a state t 2
is a simulation mapping from A 0 to A.
The formalism we have introduced allows not only for
code reuse, but also, as we show in this section, for proof
reuse by means of incremental proof construction. We
start with an example, then we prove a general theorem.
An Example of Proof Reuse
We now revisit the shared register example of Section
3. We present a parent specification of a
sequentially-consistent shared register, and describe a
simulation that proves that it is implemented by the
write through cache automaton presented in the
previous section. We then derive a child specification
of an atomic shared register by specializing the parent
specification. Finally, we illustrate how a proof that automaton
atomic write through cache implements
the child specification can be constructed incrementally
from the parent-level simulation proof.

Figure

4 presents a standard specification of a
sequentially-consistent shared register x. The interface
of seq consistent register is the same as that of
through cache. The specification maintains
a sequence hist-x of the values stored in x during an
execution. A write p
(v) request appends v to the end
of hist-x. A response read p
(v) to a read request is allowed
to return any value v that was stored in x since p
last accessed x; this nondeterminism is an innate part of
sequential consistency. The specification keeps track of
these last accesses with an index last p
in the hist-x.
We argue that automaton write through cache
of

Figure

2 satisfies this specification by exhibiting
a simulation relation R. R relates a state
t of write through cache to a state s of
seq consistent register as follows:
(t, s) 2 R ()
2 Integer) such that
-s.hist-x-
step of write through cache initiating
from state t and involving read p
(v) simulates a

Figure

4 Sequentially consistent shared register specification
automaton.
automaton seq consistent register
Signature:
Input: write p (v)
read
Output: read p (v)
State:
last p
Transitions:
eff: append v to hist-x
last p
INPUT read req p ()
OUTPUT read p (v) choose i
pre:
last p
eff: last p / i
step of seq consistent register which initiates from
s and involves read p
(v) choose hi p
, where hi p
is the
number whose existence is implied by the simulation
relation R. Steps of write through cache involving
read
(v) actions simulate steps of
seq consistent register with the respective actions.
It is straightforward to prove that R satisfies the two
conditions of a simulation relation (Definition 2.1). We
are not interested in the actual proof, but only in reusing
it, i.e., avoiding the need to repeat it.
For the purpose of illustrating proof reuse, we present in

Figure

5 a specification of an atomic shared register as a
specialization of seq consistent register. The child
restricts the allowed values returned by read p
(v) to the
current value of x by restricting the non-deterministic
choice of i to be the index of the latest value in hist-x.

Figure

5 Atomic shared register specification.
automaton atomic register
modifies seq consistent register
Transition Restriction:
OUTPUT read p (v) choose i
pre:
We want to reuse the simulation R to prove that automaton
atomic write through cache implements
atomic register. Since atomic register does not
extend the states of seq consistent register, the
simulation relation does not need to be extended, and
it works as is. In general, one may need to extend the
simulation relation to capture how the imple-
mentation's state relates to the new state added by the
specification's child.
To prove that R is also a simulation relation from
the child algorithm atomic write through cache
to the child specification atomic register we have to
show two things:
First, we have to show that initial states of
atomic write through cache relate to the initial
states of atomic register. In general, as we prove
in Theorem 4.1 below, we need to check the new variables
added by the specification child. We need to show
that, for any initial state of the implementation, there
exists a related assignment of initial values to these new
variables. In our example, since atomic register does
not add any new state, we get this property for free.
Second, we need to show that whenever R simulates
a step of seq consistent register, this step is still
a valid transition in atomic register. As implied
by Theorem 4.1, we only have to check that the new
preconditions placed by atomic register on transitions
of seq consistent register are still satisfied
and that the extension of the simulation relation is pre-
served. Since in our example atomic register does
not add any new state variables, we only need to show
the first condition: whenever read p
(v) choose i is
simulated in atomic register, the new precondition
"i holds.
Recall that, when read p
(v) choose i is simulated in
atomic register, i is chosen to be hi p
. For this
simulation to work, we need to prove that it is always
possible to choose hi p
to be -hist-x-. This
follows immediately from the added precondition in
atomic write through cache, which requires that
read p
(v) only occurs when synched p
true, and
from the following simple invariant. (This invariant can
be proven by straightforward induction.)
Invariant 4.1 In any reachable state t of atomic -
write through cache:
true =) t.cache p
Proof Extension Theorem
We now present the theorem which lays the foundation
for incremental proof construction. Consider the
example illustrated in Figure 1, where a simulation relation
from an algorithm A to a specification S is
given, and we want to construct a simulation relation
R c
from a specialized version A 0 of an automaton A to
a specialized version S 0 of a specification automaton S.
In Theorem 4.1 we prove that such a relation R c
can be
constructed by supplementing R p
with a relation R n
that
relates the states of A 0 to the state extension introduced
by S 0 . Relation R n
has to relate every initial state of A 0
to some initial state extension of S 0 and it has to satisfy
a step condition similar to the one in Definition 2.1, but
only involving the transition restriction relation of S 0 .
Theorem 4.1 Let automaton A 0 be a child of automaton
A. Let automaton S 0 be a child of automaton S such
that
be a
simulation from A to S. Let R n
A relation R c
defined in
terms of R p
and R n
as
is a simulation from A 0 to S 0 if R c
satisfies the following
two conditions:
1. For any t 2 exists a state sj nR n
(t) such that sj n
2. If t is a reachable state of A 0 , s is a reachable state
of S 0 such that sj p
(t), and
a step of A 0 , then there exists a finite
sequence ff of alternating states and actions of S 0 ,
beginning from s and ending at some state s 0 , and
satisfying the following conditions:
(a) ffj p
is an execution sequence of S.
(e) ff has the same trace as
Proof 4.1: We show that R c
satisfies the two conditions
of Definition 2.1:
1. Consider an initial state t of A 0 . By the fact that
is a simulation, there must exist a state sj pR p
) such that sj p
start(S). By property 1,
there must exist a state sj n
(t) such that
. Consider state
is in R c
(t) by definition. Also,
start(S) \Theta N 0
use the fact
that start(S 0
(Def. 3.1).
2. First, notice that the assumption on state s and
relation R c
imply that s 2 R c
(t) and that properties
2c and 2d imply that s 0
Next, we show that ff is an execution sequence of
with the right trace. Indeed, every step of ff is
consistent with trans(S) (by 2a) and is consistent
with TR (by 2b). Therefore, by definition of
(Def. 3.1), every step of ff is consistent
with In other words, ff is an execution
sequence of S 0 which starts with state R c
ends
with state R c
and has the same trace
as
In practice, one would exploit this theorem as follows:
The simulation proof between the parent automata already
provides a corresponding execution sequence of
the parent specification for every step of the parent al-
gorithm. It is typically the case that the same execution
sequence, padded with new state variables, corresponds
to the same step at the child algorithm. Thus, conditions
2a, 2c, and 2e of Theorem 4.1 hold for this se-
quence. The only conditions that have to be checked
are 2b, and 2d, i.e., that every step of this execution
sequence is consistent with the transition restriction TR
placed on S by S 0 and that the values of the new state
variables of S 0 in the final state of this execution are
related to the post-state of the child algorithm.
Note that, we can state a specialized version of Theorem
4.1 for the case of three automata, A, S, and S 0 , by
letting A 0 be the same as A. This version would be useful
when we know that algorithm A simulates specification
S, and we would like to prove that A can also simulate a
child S 0 of S. The statement and the proof of this specialized
version are the same as those of Theorem 4.1,
except there is no child A 0 of A must be
substituted for A 0 and t for tj p
. In fact, given this specialized
version, Theorem 4.1 then follows from it as a
corollary because the relation fht;
g is
a simulation relation from A 0 to S, and the specialized
theorem applies to automata A 0 , S, and S 0 .
Interface extension is a formal construct for altering the
interface of an automaton and for extending it with new
forms of interaction.
For technical reasons, it is convenient to assume that the
interface of every automaton contains an empty action
ffl and that its state-transition relation contains empty-
transitions: i.e., if A is an automaton, then
An interface extension of an automaton is defined using
an interface mapping function that translates the new
(child) interface to the original (parent) interface. New
actions added by the child are mapped to the empty
action ffl at the parent. The child's states and start
states are the same as those of the parent. The state-transition
of the child consists of all the parent's transi-
tions, renamed according to the interface mapping. In
particular, the state-transition includes steps that do
not change state but involve the new actions (those that
map to ffl).
Definition 5.1 Automaton A 0 is an interface-
extension of an automaton A if
states(A), and if there exists
a function f, called interface-mapping 1 , such that
1. f is a function from
that f can map non-ffl actions of A 0 to ffl (these are
the new actions added by A 0 ) and is also allowed to
be many-to-one.
2. f preserves the classification of actions as "input",
"output", and "internal". That is, if  2
is an input action, and f() 6= ffl, then f() is also
an input action; likewise, for output and internal
actions.
3.
Notation 5.2 Let A 0 be an interface-extension of A
with an interface-mapping f.
If ff is an execution sequence of A 0 , then ffj f denotes a
sequence obtained by replacing each action  in alpha
with f(), and then collapsing every transition of the
form (s; ffl; s) to s.
Likewise, if fi is a trace of A 0 , then fij f denotes a
sequence obtained by replacing each action  in fi to
f(), and by subsequently removing all the occurrences
of ffl.
The following theorem formalizes the intuition that the
sets of executions and traces of an interface-extended
automaton are equivalent to the respective sets of
the parent automaton, modulo the interface-mapping.
The proof is straightforward by induction using Definition
5.1 and Notation 5.2.
Theorem 5.1 Let automaton A 0 be an interface extension
of A with an interface-mapping f.
Let ff be a sequence of alternating states and actions of
A 0 and let fi be a sequence of external actions of A 0 .
Then:
1. ff 2
2.
When interface extension is followed by the specialization
modification, the resulting combination corresponds
to the notion of modification by subclassing for
extension [8]. The resulting child specializes the parent's
behavior and introduces new functionality. Specifically,
a specialization of an interface-extended automaton may
add transitions involving new state components and new
interface. The generalized definition of the parent-child
relationship is then as follows:
1 Interface-mapping is similar to strong correspondence of [38].
Definition 5.3 Automaton A 0 is a child of an automaton
A if A 0 is a specialization of an interface extension
of A.
Theorem 5.1 enables the use of the proof extension theorem
(Theorem 4.1) for this parent-child definition, once
the child's actions are translated to the parent's actions
using the interface mapping of Definition 5.1.
6 PRACTICAL EXPERIENCE WITH INCREMENTAL
PROOFS
In this section we describe our experience designing
and modeling a complex group communications service
(see [26]), and how the framework presented in this paper
was exploited. We then describe an interesting modeling
methodology that has evolved with our experience
in this project.
Group communication systems (GCSs) [3, 37] are powerful
building blocks that facilitate the development of
fault-tolerant distributed applications. GCSs typically
provide reliable multicast and group membership ser-
vices. The task of the membership service is to maintain
a listing of the currently active and connected processes
and to deliver this information to the application whenever
it changes. The output of the membership service
is called a view. The reliable multicast services deliver
messages to the current view members.
Traditionally, GCS developers have concentrated primarily
on making their systems useful for real-world
distributed applications such as data replication
(e.g., [16]), highly available servers (e.g., [5]) and collaborative
computing (e.g., [7]). Formal specifications
and correctness proofs were seldom provided. Many
suggested specifications were complicated and difficult
to understand, and some were shown to be ambiguous
in [4]. Only recently, the challenging task of specifying
the semantics and services of GCSs has become an
active research area.
The I/O automaton formalism has been recently exploited
for specifying and reasoning about GCSs (e.g.,
in [9, 11, 12, 15, 24, 28]). However, all of these suggested
I/O automaton-style specifications of GCSs used
a single abstract automaton to represent multiple properties
of the same system component and presented a
single algorithm automaton that implements all of these
properties. Thus, no means were provided for reasoning
about a subset of the properties, and it was often difficult
to follow which part of the algorithm implements
which part of the specification. Each of these papers
dealt with proving correctness of an individual service
layer and not with a full-fledged system.
In [26], we modeled a full-fledged example spanning
the entire virtually synchronous reliable group multi-cast
service. We provided specifications, formal algorithm
descriptions corresponding to our actual C++
implementation, and also simulation proofs from the algorithms
to the specifications. We employed a client-server
We presented a virtually synchronous
group multicast client that interacts with an external
membership server. Our virtually synchronous group
multicast client was implemented using approximately
6000 lines of C++ code. The server [27] was developed
by another development team also using roughly 6000
lines of C++ code. Our group multicast service also
exploits a reliable multicast engine which was implemented
by a third team [34] using 2500 lines of C++
code.
We sought to model the new group multicast service in
a manner that would match the actual implementation
on one hand, and would allow us to verify that the algorithms
their specifications on the other hand. In
order to manage the complexity of the project at hand
we found a need for employing an object-oriented approach
that would allow for reuse of models and proofs,
and would also correspond to the implementation, which
in turn, would reuse code and data structures.
In [26], we used the I/O automaton formalism with the
inheritance-based incremental modification constructs
presented in this paper to specify the safety properties
of our group communication service. We specified four
abstract specification automata which capture different
GCS properties: We began by specifying a simple GCS
that provides reliable fifo multicast within views. We
next used the new inheritance-based modification construct
to specialize the specification to require also that
processes moving together from one view to another deliver
the same set of messages in the former. We then
specialized the specification again to also capture the
Self Delivery property which requires processes to deliver
their own messages. The fourth automaton specified
a stand-alone property (without inheritance) which
augments each view delivery with special information
called transitional set [37].
We then proceeded to formalize the algorithms implementing
these specifications. We first presented an algorithm
for within-view reliable fifo multicast and provided
a five page long formal simulation proof showing
that the algorithm implements the first specification.
Next, we presented a second algorithm as an extension
and a specialization of the first one. In the second al-
gorithm, we restricted the parent's behavior according
to the second specification, i.e., we added the restriction
that processes moving together from one view to
another deliver the same set of messages in the former.
Additionally, in the second algorithm, we extended the
service interface to convey transitional sets, and added
the new functionality for providing clients with transitional
sets as per the fourth specification. By exploiting
Theorem 4.1, we were able to prove that the second algorithm
implements the second specification (and therefore
also the first one) in under two pages without needing
to repeat the arguments made in the previous five
page proof. We separately proved that the algorithm
meets the fourth specification. Finally, we extended and
specialized the second algorithm to support the third
property. Again, we exploited Theorem 4.1 in order to
prove that the final algorithm meets the third specification
(and hence all four specifications) in a merely two
and a half page long proof.
We are currently continuing our work on group commu-
nication. We are incrementally extending the system
described in [26] with new services and semantics using
the same techniques.
A Modeling Methodology
Specialization does not allow children to introduce behaviors
that are not permitted by their parents and does
not allow them to change state variables of their par-
ents. However, when we modeled the algorithms in [26],
in one case we saw the need for a child algorithm to
modify a parent's variable. We dealt with this case by
introducing a certain level of non-determinism at the
parent, thereby allowing the child to resolve (specialize)
this nondeterminism later.
In particular, the algorithm that implemented the second
specification described above sometimes needed to
forward messages to other processes, although such forwarding
was not needed at the parent. The forwarded
messages would have to be stored at the same buffers
as other messages. However, these message buffers were
variables of the parent, so the child was not allowed
to modify them. We solved this problem by adding a
forwarding action which would forward arbitrary messages
to the parent automaton; the parent stored the
forwarded messages in the appropriate message buffers.
The child then restricted this arbitrary message forwarding
according to its algorithm.
We liken this methodology to the use of abstract methods
or pure virtual methods in object-oriented methodol-
ogy, since the non-determinism is left at the parent as a
"hook" for prospective children to specify any forwarding
policy they might need. In our experience, using
this methodology did not make the proofs more complicated

7 DISCUSSION
We described a formal approach to incrementally defining
specifications and algorithms, and incorporated an
inheritance-based methodology for incrementally constructing
simulation proofs between algorithms and
specifications. This technique eliminates the need to
repeat arguments about the original system while proving
correctness of a new system.
We have successfully used our methodology in specifying
and proving correct a complex group communication
service [26]. We are planning to experiment with our
methodology in order to prove other complex systems.
We have presented the technique mathematically, in
terms of I/O automata. Furthermore, the formalism
presented in this paper and the syntax of incremental
modification is consistent with the continued evolution
of the IOA programming and modeling language. Since
IOA is being developed as a practical programming
framework for distributed systems, one of our goals is
to incorporate our inheritance-based modification technique
and approach to proof reuse into the IOA programming
language toolset [17, 18].
Future plans also include extending our proof-reuse
methodology to a construct that allows a child to modify
the state variables of its parent. Other future plans
include adding the ability to deal with multiple inher-
itance. In all of our work, we aim to formulate and
extend formal specification techniques that would be
useful for practical software development.

ACKNOWLEDGMENTS

We thank Paul Attie, Steve Garland, Victor Luchangco
and Jens Palsberg for their helpful comments and suggestions



--R

A Theory of Objects.
The existence of refinement mappings.
ACM 39(4)
On the formal specification of group membership ser- vices
Fault tolerant video- on-demand services
An object-oriented approach to verifying group communication systems
Middleware support for distributed multimedia and collaborative computing.
An Introduction to Object-Oriented Program- ming
An Adaptive Totally Ordered Multi-cast Protocol that Tolerates Partitions
A denotational semantics of inheritance and its correctness.

A dynamic primary configuration group communication service.
Data Refinement Model-Oriented Proof Methods and their Comparison

Specifying and using a partionable group communication ser- vice
Fast replicated state machines over partitionable networks.
Foundations of Component Based Systems
IOA: A Language for Specifying
Optimizing Layered Communication Protocols.
Formal methods for developing high assurance computer systems: Working group report.
The generalized railroad crossing: A case study in formal verification of real-time systems
On the need for 'practical' formal methods.
Wrapper semantics of an object-oriented programming language with state
Specifications and proofs for ensemble layers.
Inheritance in Smalltalk-80: A denotational definition
A client-server approach to virtually synchronous group multicast: Specifica- tions
A Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs
Multicast group communication as a base for a load-balancing replicated data service
Generalizing Abstraction Functions.
Distributed Algorithms.
Robust emulation of shared memory using dynamic quorum-acknowledged broadcasts
An introduction to In- put/Output Automata
Objects as closures: Abstract semantics of object-oriented languages
Implementation of Reliable Datagram Service in the LAN environment.
Proving correctness with respect to nondeterministic safety specifications.
Modular reasoning in the presence of subclassing.
Group Communication Specifications: A Comprehensive Study.
I/O automaton model of operating system primitives.
--TR
Objects as closures: abstract semantics of object-oriented languages
Inheritance in smalltalk-80: a denotational definition
The existence of refinement mappings
Proving correctness with respect to nondeterministic safety specifications
A denotational semantics of inheritance and its correctness
Modular reasoning in the presence of subclassing
An introduction to object-oriented programming (2nd ed.)
Specifying and using a partitionable group communication service
A dynamic view-oriented group communication service
Eventually-serializable data services
Distributed Algorithms
A Theory of Objects
Data Refinement
Wrapper Semantics of an Object-Oriented Programming Language with State
Multicast Group Communication as a Base for a Load-Balancing Replicated Data Service
A Dynamic Primary Configuration Group Communication Service
Specifications and Proofs for Ensemble Layers
On the Need for Practical Formal Methods
Robust emulation of shared memory using dynamic quorum-acknowledged broadcasts
Fast Replicated State Machines Over Partitionable Networks
Formal Methods For Developing High Assurance Computer Systems
A Client-Server Approach to Virtually Synchronous Group Multicast
Optimizing Layered Communication Protocols
Fault Tolerant Video on Demand Services
A Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs

--CTR
Sarfraz Khurshid , Darko Marinov , Daniel Jackson, An analyzable annotation language, ACM SIGPLAN Notices, v.37 n.11, November 2002
Keidar , Roger I. Khazan , Nancy Lynch , Alex Shvartsman, An inheritance-based technique for building simulation proofs incrementally, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.1, p.63-91, January 2002
system modeling/verification;specialization by inheritance;simulation;refinement;interface extension