Pushouts in Software Architecture Design
T. L. Riché

National Instruments
Austin, TX, USA
taylor.riche@ni.com

R. Gonçalves

B. Marker and D. Batoryrgoncalves@di.uminho.pt{bamarker,batory}@cs.utexas.edu

Departamento de Informática
Universidade do Minho
Braga, Portugal

ABSTRACTA classical approach to program derivation is to progressively extend a simple specification and then incrementally refine it to an implementation. We claim this approach is hard or impractical whenreverse engineering legacy software architectures. We present acase study that shows optimizations and pushouts—in addition torefinements and extensions—are essential for practical stepwise development of complex software architectures.

Categories and Subject Descriptors
D.1.2 [Programming Techniques]: Automatic Programming; D.2.2[Software Engineering]: Design Tools and Techniques; D.2.11[Software Engineering]: Software Architectures; F.3.3 [Logics
and Meanings of Programs]: Studies of Program Constructs

General Terms
Design, Theory

Keywords
MDE, Software Architectures, Program Derivation, Pushouts

1.

INTRODUCTION

At a recent NSF workshop on the Future of Software Engineering [45], there was consensus on the need for automated support
for program evolution—for the obvious reason that programs canbe very complicated structures whose safe and correct manipulation
should yield a major improvement in the software lifecycle [24].
Workshop discussions revealed an interesting open problem. Classical approaches to program development define the spec of a simple program A1 and progressively extend it with additional functionality until the desired, fully-formed spec A4 is completed. Then
A4 is incrementally refined to an implementation, arriving at program D4 (Figure 1a) [53]. A variation is after each extension, an
implementation is produced by “replaying derivations” [6, 24, 38].
After the workshop it was obvious (to us) that how one accomplishes derivation replay in the presence of extensions is not wellunderstood.

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
GPCE’12, September 26–27, 2012, Dresden, Germany.
Copyright 2012 ACM 978-1-4503-1129-8/12/09 ...$15.00.

Dept. of Computer Science
University of Texas at Austin
Austin, TX, USA

A1

A2

A3

A4

A1

A2

A3

A4

B4

B1

B2

B3

B4

C4

C1

C2

C3

C4

D1

D2

D3

D4

D4

(a) Classical Approach(b) Incremental Approach

Figure 1: Paths
We are exploring transformation-based derivations of pipe-and-filter
architectures to reverse engineer designs of legacy architectures.
Our goals are to reveal a process to derive architectural designs andto reconstruct these applications directly from our derivations.
We discovered that prior work on refinement under-appreciates
two key ideas. First, optimizations are essential—one must erase
modular boundaries in order to achieve designs that have non-functional properties (e.g. efficiency or fault-tolerance). Optimizations
are not always part of refinement methodologies [27, 30, 38, 59].
Second, architectural designs can be very complicated. We foundit impractical to refine fully-elaborated specifications—the refinements were too complex to understand and explain. Instead, we
followed an incremental path (Figure 1b) that (a) refined a simple
spec to its implementation at different levels of abstraction (designs
B1 , C1 , D1 ), and then (b) incrementally extended these implementations using pushouts (completing a directed squarefrom anincomplete square ) to complete the commuting diagram of Figure 1b [47]. Each step (refinement, optimization, extension) was
relatively easy to understand, allowing us to comprehend how alegacy application worked despite its complexity. Pushouts were
the key for us to understand how to “replay derivations.”
We present a case study of how we reverse-engineered the architecture of a complex, state-of-the-art asynchronous crash-fault
tolerant server. We demonstrate the essential role of optimizations
and pushouts—in addition to refinement and extension—by showing how we recover architectures of two versions of the system(both of which had no formal architectural description prior to ourwork): first a synchronous server and then an extension to an asynchronous server.
Stated differently, without optimizations and pushouts, we could
not have reengineered legacy architectures nor could we have forward-engineered (reconstructed) them. Our conclusion is that optimizations and pushouts are essential for practical stepwise development of complex software architectures.

2.

REFINEMENTS AND OPTIMIZATIONS

A pipe-and-filter (PnF) architecture is a directed multigraph ofboxes and connectors that implements a system. A box is a component with input and output ports. A connector is a communication
path for messages drawn in the direction of dataflow from an output
port to one or more input ports [50].

© ACM, 2012. This is the author’s version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published inProceedings of the 11th International Conference on Generative Programming and Component Engineering. http://dx.doi.org/10.1145/2371401.2371415

(b)

P

filterb

LEFT

FILTER(a)P

FILTERQ(c)

FILTERP(b)P

filterb

Q

SPLIT

H
MERGE

mapreducefilterH
F (Figure
H It consists
F-1 2a).
H architectureFH
F-1 is Han example
A filterof asingle box FILTER that takes a stream of photographs P as input,
examines each photographp in P, and outputs
p only if (c)some crite(a)(b)
ria is satisfied. A shorter stream Q is produced. FILTER may haveother parameters, such as a photograph type and filtering criteria.
We elide these details.
An architectural transformation is a mapping (a multigraph rewrite) of an input architecture to an output architecture. We use
three types of transformations: refinement, optimization, and extension. We discuss the first two now.

Refinement

Suppose there are multiple (but semantically equivalent) filteringboxes, filtera and filterb , each with its own distinct performance characteristics. A transformation could replace the FILTER
box of Figure 2a with the filterb box resulting in Figure 2b. Another transformation replaces the FILTER box of Figure 2a with its
map-reduce counterpart in Figure 2c, showing that an input stream
can be split into substreams, each substream is filtered in parallel,
and the output substreams are merged [16].
The collection of such transformations used in a domain forms
a graph grammar: let A be an interface (a box that defines only the
input/output ports and—at least informally—box semantics), andlet g1 , g2 , . . . denote architectures (multigraphs) and/or primitive
boxes that implement A:
A : g1 | g2 | . . . ;As an example, if FILTER of Figure 2a is a filter interface and everything else is an implementation, we have:
FILTER : filtera | filterb| mapreducefilter( SPLIT, FILTER, MERGE ) ;where mapreducefilter( SPLIT, FILTER, MERGE ) is the architecture of Figure 2c that is parameterized by implementations of
the SPLIT, FILTER, and MERGE interfaces. Replacing an interface
with an implementation is refinement [59].
Of course, the gi multigraphs can reference other interfaces whichhave their own productions (implementations). The set of multigraphs that can be constructed by substituting implementations forinterfaces defines the language or domain of systems that can besynthesized by refinement.
In general, a refinement has preconditions to satisfy before it
can be applied. Consequently our grammars are not context-free.
Recording such preconditions is indeed part of our work; we elide
these details.

Optimization

Refinements alone are insufficient to build efficient systems. Consider the following grammar, where uppercase names are interfaces
and lowercase names are components:
A : a B c | ... ;B : b | ... ;

RIGHT

F-1

F

FILTER

IDENTITY

H

H

F-1

F

H

(b)

(a)

FILTER

IDENTITY

2.2

mapreducefilter

H

Q

Figure 2: Pipe and Filter Architectures

2.1

Q

(c)

Figure 3: Architecture Optimizations
A sentence of this grammar is abc. Suppose composition bc implements interface Z:
Z : bc | q ;Further, domain experts know that composition bc is inefficient andcan be replaced by box q, which is faster. This is accomplished by
abstracting sentence abc to aZ and then refining to a faster program by replacing Z with q to yield aq. Abstraction followed byrefinement is the essence of architectural optimization. The pairingof bc arises because c comes from a refinement of A and b comesfrom a refinement of B. Dissolving modular boundaries exposes
inefficiencies which can be removed by optimizations.
Figure 3a is an example. Modular boundaries are indicated bydashed lines. The LEFT box processes stream H by box F. The
RIGHT box immediately processes its input by box F 1 , the inverseof F. Figure 3b dissolves these boundaries, exposes the inefficiency,
and reveals the IDENTITY abstraction of which (F followed by F 1 )is an implementation. Figure 3c is the optimized architecture.
With optimizations, our grammars become a set of bi-directional
rewrite rules (interface , implementation pairs) called a Thue
System [8].

2.3Application to Case Studies

The PnF architecture of our case study was never conceived interms of transformations and was not built with the aid of software architectural models. However, the novelty, indeed genius, of
its design can be expressed in terms of a sequence of transformations that were implicitly used by their authors. It was built over a
five month period during which its authors used less rigid engineering approaches. The authors did what felt natural, but effectively
used transformations. (Exposing these transformations and making
them explicit is one of our contributions). There may be no a priori
reason or justification for why the authors chose particular transformations, other than they were necessary for that system or thatthey introduced a novel algorithm or protocol.
Further, our explanations are no substitute for domain expertise;
they are intended to complement, encode, and structure domain
knowledge for others to follow. Expressing designs by transformations may be novel to domain experts, but the end result is rarely
surprising to them. Further, the assumptions we use are standard
fare for the domain. On the other hand, non-experts may find theassumptions or the choice of transformations unintuitive. In any
case, our approach offers a simple and effective way to reveal architectural details of PnF applications incrementally and be able torecreate these applications from these descriptions.

3.

THE SCFT ARCHITECTURE OFUPRIGHTOur interest in PnF architectures originally stemmed from a reverse-engineering effort to understand Figure 4, which is a portionof the PnF architecture of Upright, a state-of-the-art Asynchronous
Crash-Fault Tolerant (ACFT) server [14]. We could not explain orderive this architecture directly. Instead, we first derived a simpler
architecture for a Synchronous Crash-Fault Tolerant (SCFT) server.
In later sections, we extend our SCFT design to an ACFT design.

In

Om

C
In

Hn

Tn1

T1m

Tnm

Tnm

Om

Gm

C

.

C
Qr1

Qrn
C1

ver

F1

C2

Ra1

F2

Cn

Qa1

Ra2

...

Qa2

...

I1 Fn

Rs1

Qs1

Rs2

TQs
11

...

Ram

G

Qak

I1

2

H1

...
T1m

Rsk

O1

T

Qsn

In

H

E

Tn1

Hn

Figure 4: Asynchronous Crash Fault Tolerant Architecture
Tnm
In

3.1

E

The technical objective of SCFT is to eliminate Single Points of
E·SOF
E·WServer
E extend
Failure(SPoF) by
replicating functionality[49]. An SPoF is the
WServer
failure of a single box that causes thenewKey
entire server abstraction to(a)fail. Our initial design (Figure 5b) has(b) three SPoFs: the serializer B, the server S, and the demultiplexer C. Client failures neverT11 cause a server abstraction to fail as SCFT servers should expect and
G1
Ohandle1
E·SOF We show
E·WServer
gracefully
non-responsive clients.
in the followWServer
Tn1 SOFing sections how Figure 4 is an extended, newKey
refined, and optimized
T1m implementation of Figure 5b that has no SPoFs and is recoverable.
A

SOF

Qr2

Om

(a)

(b)

Basic Request Processing

Tnm
(a)

Gm

3.2.1

R

(a)
G

T

I1

H

In

R

C2

(b)

... H1

In

Hn

T11

T1m

Tn1

Tn1

T1m

Tnm

Tnm

Cn

Om

S

T11

G1

C2

3.2
SOF

C1

Synchronous CFT
C2

L

(a)

C2

A2

F

S

...

...

...

Cn

Cn

An

Qa

Figure 6: After the List Refinement
Sort

WebServer

ESort

C1

Replication Refinements

C

EWebServer

F1

newKey

(a)

A1

Qa1

(b)

An

A1

C2

F

A2

WebServer

Qa

S2

...

...

Cn

Am

Sk

Figure 7: Replicated Agreement and Server Boxes
A1

C1

Qr1

S1

(a)

F1

Ra1

Qa1

Rs1

Qs1

newKey

C2

F2

Ra2

Qa2

Rs2

Qs2

(b)

...

EWebServer

Qak

Qs

C1

ESort

...

S1

LEFT
MIDDLERIGHTFirst consider
the replicating-serverrefinement RepS.
It repliQr
A2Qa
S2 S1 . . . SkQs
catesC2the server FS k-times,
indicatedby boxes, and adds2...
three... new boxes: , ...B, and Qs. Box
reliably
broadcasts Qr
ann
Cn
incoming
message to Aeach
server replica: if Sone
server replica rem
k
C1 receive
F1 the message—such
Ra1
ceives a message, then all replicasa
EWebServer
strong guarantee is necessary for correctness. Replicas receive the1 Replicating a stateless application is easy: consistency across newKeymessage, update their state, and send
C2 responses.
F
Ra2 all Qs
reC1
F1
A1
Qa1 2
S1B serializes
1
replicas is guaranteed by the fact (thatofidentical
responses.
Once) the replicas never change.
( ) sponses and box Qs collects a quorum...
...
2 CFT servers must uphold two properties: safety and liveness.
C2
F2
A2
Qa2
S2number of S repliQs2
Qs receives
matching
responses
from a sufficient
(b)
C1
Cn
Fn ...
Ran
Loosely, safety means
the server is always in a “good” state, for...
... transmits a single... response... client,cas, Qs
to thethus maintaining
varying definitionsC2of “good”, andliveness means that the serverS
the abstraction
Cn
Fn of a single
Am server S.
Qak
Sk
Qsn
eventually makes progress [43]. Upright provides a serializable
Now consider the Paxos refinement of box L [36, 37]. When aview of RPAs [46];... serialization proofs of Upright’s protocols areclientsubmits a message, a forwarding box (F) receives it and deCngiven in [34]. Further, Upright’s protocols uphold a liveness proplivers the message to any or all of the m identical agreement boxes
erty called “eventual liveness” [14]. As consensus in an asynchronous system is impossible [20], the existence of occasional peA1 . . . Am . Each A box implements an agreement protocol to guaranriods of a well-behaved network is assumed, allowing both SCFT
tee a quorum-decided linear order in which client messages should
C1 to make progress.
and ACFT serversS
be processed. A replicas communicate with each other to determine
3 We assume that each box executes on its own machine. Normally,
the next client message to process. Each A replica votes, sending
C2
LS
multiple boxes are
mapped to a single machine. The rule for maQr1...
chine failure is simple: if a machine fails, all boxes on that machineis assumed to not occur. Work on Byzantine Fault Tolerance (BFT)
Qr2
Cn
fail.
relaxes these assumptions [13,14, 35]. In any case, the mapping of
4 All requests and boxes are assumed benign. Malicious behavior
a vanilla client-server designQrton a SCFT design is unaffected: BFT(or even benign behavior outside the accepted application protocol)
designs extend SCFT designs.
Sort

Qa2

S

...

S

ber of failures. A crash failure...occurs when a box stops processing(a) messages—no messages pass C(b) a failed box and a failed box
throughncannot create new messages. The failure of network boxes—B, C,(reliable broadcast [43]), and • (broadcast)—are treated idenE·WServer meaning thatto software boxes. FailureE·SOF
is self-contained,
SOF tically WServer
3, 4
failures do not propagate acrossbox
boundaries.
newKeySort
WebServer
ESort

Fn

L

Crash fault Etolerance
is theE·SOF
ability ofE·WServera service to survive a numextend
WServer
newKey

E

L

Cn

Om

Qa

S

O1

Figure 5: Unrolled Cylinder Topology

C

A1

C1

C1
Gm

A2

F

C2 and RepS,
F2
The next transformations, Paxos
replicate Aboxes
to2
improve system availability, i.e. ...to make the server abstraction...
more resilient to crashes. See Figure 7.

C1

O1

I1

C2

C1

3.2.2

(b)

List Refinement

C

.

1

The List(b)transformation
maps box S to an architecture where
C1...
there is a single box L between the...clients and server. L implements
CS
2C
an ordered list of messages, collecting
messages from Aclients
andnnpassing messages one...at a time to the server. In effect L makes theCn materializing a placeholder for subsequent
network queue explicit,
refinements. Figure 6 shows the architecture after applying List.

Request-processing applications (RPAs) have multiple clients
sending requests (a.k.a. messages) to a server. Client requests canread or write the server’s internal state, which persists across requests. ThatWServer
servers have stateis important: crash-fault
tolerance
E·SOF
E·WServer
E extend
SOF(CFT) of non-stateful servers is trivial.1
newKey
RPAs have a cylinder topology representing the cyclic flow of(a)request-response.
We unroll the cylinder (Figure 5a)(b)by breaking
the seam along dotted lines. Figure 5b shows a typical architecture with clients C1 . . . Cn and server S. Each client sends messages
to the server. Messages from different clients are serialized
intoE·WServer
E·SOF
SOF
WServera single stream by B. The server receives each message, updates
newKeyits state, and then sends its response. Responses are demultiplexed
into multiple output streams, one per client, by C. Response messages wrap around the dotted lines. 2
(a)

C1

Om

C

Cn

...
Fn

Ram

Qak

...

...

Rsk

Qsn

Qa1
Qa2
Qak

C

.

C

Qa2
...
Qak

its “next” message to the quorum box Qa. Qa forwards a single
message to the server once it receives identical messages from a
sufficient number of replicas. In this way, Paxos maintains the
behavior of and interface to a single L box.
The degree of A and S box replication—values m and k—dependon the number of faults f to tolerate and the agreement protocol.
Common assignments set m = 2f + 1 and k = f + 1. 5
The Paxos and RepS transformations commute as the order inwhich they are applied does not matter. However, both must be
applied to guarantee that the system tolerates the failures of up tof server and f agreement boxes. Figure 7 is the result of applying
Paxos and RepS to Figure 6.

3.2.3

m

C1
C2

S1

MIDDLE

A2

F

Qa

RIGHT

S2

...

...

...

Cn

Am

Sk

Qs

Figure 8: Abstractions with Multiple SPoFs
F1

A1

Qa1

F2
...
Fn

Figure 10: The Ra Rotation
The MIDDLE abstraction of Figure 8, replicated in Figure 11a,consists of the box sequence (B, Qa, ). Transformation Rb is apair of rotations that modify the order (B, Qa, ) to (B, , Qa) (Figure 11b) and finally to ( , B, Qa) (Figure 11c). That is, instead oftaking a quorum of responses from A replicas and reliably broadcasting the result, the results of all A replicas are reliably broadcast
and a quorum is taken at each server replica. The property that aquorum-decided request from replicated A boxes is delivered to allserver replicas is preserved by Rb .
MIDDLE

R

Qs1

I1

O1
G

T

H

Qr1 I1

Om Qr2

In

Qrn

er

C1

F1

C2

F2

Cn

E

(a)

T11

T11

T1m

Tn1

Tn1

T1m

Fn

G’1

In

H’n

Ra1

Qa1

TnmRs

Ra2

Qa2

Rs2

Ram

Qak

...
Cn

(c)

(d)

MIDDLEMIDDLE

Qa1

Qa1

Qa2

Qa2

...

...

Qak

Qak

L

S

Figure 11: The RAb1 Optimization
C

1

Rsk

Tnm

G’m

Om
Qs1

S1

Qs2
...
Qsn

Rb includes one more optimizationthat is well-known to domain
A2
Qa
S2
C2
F
experts. Reliable broadcast is very expensive.7 By replicating at
...
...
...
LEFT
each of the (a)Ai boxes, we can(b)take advantage of the fact thatquoLEFTC
Fn1
rums are taken at each server and replace
the reliable broadcast
Am
Sk boxF
with the normal (unreliable)
network broadcast box • that is simF2
ple to implement. The abstraction in Figure 11d now contains no...
SPoFs, and also represents a standard
and efficient way to impleAF1n
S1ment a reliableC1crossbarLEFT[14].
MIDDLE
Similarly, transformation Rc is a pair of rotations that is applied
Qa the box sequence
S2
C2
to the RIGHT abstraction
in FFigure A8,2 which maps
...
...
...
(B, Qs, C) to (B, C, Qs) and then to (C, B, Qs), thereby eliminating
Cn 12 is the result of
all SPoFs. Figure
applying
R–R
to
Figurea c
Am
Sk 8. Itis the PnF architecture of Upright’s SCFT design.
7 Experts often use an agreement cluster to implement reliablebroadcast.
C1
F1
A1
Qa1
S1

C2

C1
C2

...
Qak

O1

5 Yin et al. explain the difference
E·SOF
in replicaE·WServercount by noticing thatE extend
WServerthe quorums necessary to prove the protocols
correct are larger for
newKeymessages coming from the agreement portion (Qa) than for mes(a) sages coming from the execution (Qs) (b)[60]. Since a typical server
requires more computational resources than agreement, thus needing a more powerful and expensive machine, using fewer server
replicas in an architecture is desirable.
E·SOF
E·WServer
SOF 6 Readers
WServer
will recognize this as commuting diagram G · H = H0 · G0 .
newKeyThe sequential composition of G and H is replacedwith a crossproduct of H0 and G0 : the end result is two different implementationsof the same abstraction.

(b)

Qa2

1

...
Figure ...9: Rotation Optimization

...

SOF

H’1

MIDDLE

Qa

R

(b)

(b)

Qa1

S1

C2 is how
F2 SPoFs wereA2 removed from
QaUpright:
S2 Figure 9a shows
Qs2
Here
2
... T
... G consumes n streams...
... a single streamthat box
I1 . . . In to...produce
whichCnis input
turn, H outputs
O1 . . . Om . Let
Fn to box H. AIn
Qakm streams
Sk
QsnR
m
be interface that G followed by H implements. A rotation swaps the
positions of G and H (possibly replacing them with slightly different
operations H0 and G0 ) and replicates them, providing yet another
implementation of R.6

(a)

F1
F

(a)

C1

LEFT

(b)
LEFT

A1

LEFT

(d)

(a)

Optimizations

Our original architecture of Figure 5b had three SPoFs; our current design has eight. (From left to right in Figure 7, they are theB, F, B, Qa, , B, Qs, and C boxes.) Here is where refinement isinsufficient to derive our target architecture; modular boundaries
S
must be broken to removeL SPoFs.
A1 in Section 2.2, we Sdissolved
Exactly
as explainedboundaries
1
C1
in Figure 7 to produce Figure 8 and identify three new abstracA2
Qa boxes, all
S2 of which Qs
F
2tionsCthat
circumscribe
two or three
are SPoFs.
...
...
For example
the LEFT...abstraction contains SPoF
boxes B and F.
Cn contains threeAmSPoF boxes (B, Qa, andSk
MIDDLE), and the RIGHT
abstraction contains three SPoF boxes (B, Qs, and C).

O1

(c)

MIDDLETo see a real example
of a rotation, consider the MIDDLE
LEFT abstractionof Figure 8, which we show Qa
again
in Figure 10a comprising
Qa1 the se1
quence (B, F). The Ra rotation swaps the order of these boxes (seeQa2 once for each client andQa
Figure 10b). Box F is replicatedB2 is replicated once for each Ai . That...is, instead of serializing all... requests
and then forwarding, client requests
are immediately forwarded
and
Qak
Qak
then serialized before each A replica. The property that each client
request is sent to a subset of A replicas is preserved by Ra . As expected, the interface of n input channels and m output channels ismaintained. But now, F and B boxes are no longer SPoFs in Figure 10b.

F2

...
S

Cn

Fn

Qs

RIGHT
Qs

Qs

A2

Qa2

S2

...

...

...

Qs

...

Am

Qak

Sk

Qs

C1

S1

1

C2

F

A2

Qa

S2

...

...

...

Cn

An

Sk

Qs

Figure 12: Synchronous Crash Fault Tolerant Architecture

A pushout is a completion of the commuting diagram of Figure 13. Given refinement or optimization A ! B and extension
AE, the goal is to determine architecture F so that E ! F is arefinement or optimization and B F is an extension.9
We use pushouts to map Upright’s SCFT architecture to its corresponding ACFT architecture in the next section.

3.2.4

5.

C1

F1

A1

Qa1

C2

F2

A2
...
Am

...
Cn

Fn

S1

Qs1

Qa2

S2

Qs2

...

...

...

Qak

Sk

Qsn

Recap

We used the architecture of Figure 12 to reimplement Upright’s
SCFT design. More detailsQrabout model validation are postponed
until Section 5.6. Our next Qr
task is to extend the SCFT architecture
to an ACFT architecture (i.e. mapping from Figure 12 to Figure 4).
1
2

Qrn

WebServer

(a)
I1
In

4.

Qa
Rs
Qs
PUSHOUTS AND EXTENSIONS
C1

F1

Ra1

1

1

1

(b)
C2
Ra2
Qa2 T11 Rs2
2Think
of aF2 refinement
asI a verticalmappingT11
fromanQsinitial
arH1
G1 ... O1
1
...
...
...
O1
chitecture A to a resultant
architecture B.
T1mWe also
Tn1need transformaCTn
Ran
Qak
Rsk
Qsn
G thatH Fn
tions
extendarchitectureswith morefunctionality.
Extensions
Tn1
T1m
Om
are horizontal mappings,
suchasmappingarchitectureA
toOarchiIn
Hn
Gm
m
Tnm
Tnm
tecture E (Figure 13).
extensionErefinement

A

SOF

WServer

E extend

B
E·SOF

FE·WServer

pushout
newKeyFigure 13:(b)Pushout

(a)

E

SOF

(a)

An architectural extension augments an architecture by adding
new functionality and ports to existing boxes, generalizing connecE·SOF
E·WServer
tors,WServer
and adding new boxes and connectors. In software productlines, extensions are called features [29].newKey
A common special caseof extension is box extension, where new capabilities and ports are(a) a box is equivalent to(b)adding one oradded to a box. Extending
more features, which can be accomplished by preprocessors (e.g.
#ifdef(b)inclusionC1of extra code) or by more sophisticated means [3,5, 31]. Connectors can also be extended (e.g. messages of type M
C2 extension transmits
S
are transmitted; ana subtype T of M). We write...
X Y to mean that X is extended to Y.
Figure 14 illustrates
architectural extension a b. Figure 14aCnshows architecture a with a Sort and WebServer box. The WebServer takes sorted tuples and creates a webpage of sorted results.
Figure 14b shows an extended architecture b that permits sort keys
to be altered Cat1 run time. Sort and WebServer are extended withnew ports (Sort
ESort and WebServer
EWebServer) andC2LSa feedback connector labeled newKey is added. A newKey message changes...the key that ESort uses to sort incoming tuples (e.g.
Cn last names to ID numbers in a patient database or
switching fromartists to album titles in a music player).
( )

Sort

WebServer

( )

ESort

EWebServer
newKeyFigure 14: Architecture Extension ab

Refinement is different than extension. Refinement preserves semantics; it maps an interface to a streaming architecture that implements that interface. The interface is not altered and new connectors external to it are not added. In contrast, extension enhances
the semantics of an architecture by elaborating existing boxes withnew ports, new functionality, and new boxes and connectors.8
8 Interestingly, well-known tools for data flow architectures, like

THE ACFT ARCHITECTURE OFUPRIGHT

Failure is permanent in an SCFT architecture. If a box fails, it
no longer responds and will never respond again. An SCFT architecture supports the failure of f boxes. When the limit is exceeded,
the entire system is in a failed state, the one-server abstraction isviolated, and safety and liveness are no longer guaranteed.
In this section, we explain how domain experts relaxed restrictions on liveness. An ACFT architecture guarantees liveness evenwith an occasional poorly behaved network or temporary box failS1
ure (andC1always guaranteesA1safety), assuming the network
eventually enters a sufficiently long well-behaved period. That is, liveness
A2
Qa
S2
C2
F occasionalQs
is guaranteed
even with
network
asynchrony.
... situations where a client... sees an un... ACFT limits theIn effect
A3
A2
A4
A
responsive
Cn1 server abstraction.
Am The mechanisms thatSksupport asynchrony also allow the architecture to mask some failures by enabling a box to be restarted and catch up. A box that fails andB3 albeit Bslow.
B2 correct,
recoversB1is considered
The other boxes will
4
1
continueC1to make progress;A1 a recovering box may Snotbe able tocatch up immediately. If other boxes fail, the remaining servers
A2Qa
S2
C2 to wait forFthe recoveringQs
may have
servers
C3
C
C2
C4 to catch up (as required...
... 1 boxes), atby quorum
which...point
the system
can resumeservicingclient requests[14]. Note:Amboxes may still crash andCn
Sk enter a state
where they will never again process requests; asynchrony support
D3
D1 all failures.
D2
D4
cannot mask

5.1

(c)
C
F
Road
Map
1

1

A1

Qa1

S1

FigureC 15 showsa road map(commuting diagram)ofwhere we
F2
A2
Qa2
S2
2
are and where we are going. We began with the topmost left node
...
...
...
...
(labeled Figure 5b) and incrementally refined and optimized downCn we reachedFnAm
Qa(Figure
Sk 12). In thekward until
the bottommost
left node
next sections, we use extensions Async0 . . . Async3 to map each of
the architectures on the left to corresponding architectures on theright. The dashed vertical arrows in Figure 15 are extended refinements and optimizations (List RList, Paxos RPaxos, etc.)that complete the commuting diagram.
Fig5bStart
HereAsync0

Qr1

List

Qr

Fig6

2
Async
1

Paxos  RepS Qrn

F1 Fig7

C1
End
Here

C2

F2

...
Cn

Fn

Ra1

Async2

Ra2
...

Ram

Qs2
...
Qsn

Fig16
RList
Fig17
RPaxos  RRepS

QaFig18
1

Rs1

Qs1

Ra  R b  Rc  Rd

Ra  Rb  Rc
Fig12SCFT

Qs1Async3

Qa2

Rs2

Fig19
ACFT

...

...

Qak

Rsk

Qsn

Figure 15: Roadmap in Our ACFT Designs
LabVIEW [44], Weaves [23], Fractal [10], and Click [32] support
refinement, but not extension and not optimization. Our use of
the terms refinement and extension is consistent with that used informal methods [52].
9 The objects of this category are designs of a system at different
levels of abstraction and with different functionality.

Qs2

5.2

Asynchronous Extension Async0

Server Replication.

When the recoverable server RSb of Figure 17 is replicated, itneeds to communicate with other replicas. The reason lies in therecovery algorithm for replicated servers: when a replica crashes,other servers continue to make progress. When the failed server
recovers—it may be behind—other client messages may have beenprocessed in the interim. For the failed server to catch up, it must
fetch checkpoint state from other replicas.
Extension Async2 maps each server box S of Figure 7 to a recoverable server box RSg , S RSg . The server box is extended toaccount for server recovery (as RSb , discussed above) and for thefollowing situation. After processing a fixed number of client messages, the agreement box asks the server for its current checkpoint.
The agreement box can only accept a checkpoint if it receives aquorum of matching checkpoints from server replicas.10 Further,when a server crashes and attempts to recover, it asks the agreement
box for the latest checkpoint. This “Help, I need to recover!” message comes from just one server, and the agreement box does not
wait for a quorum (as one will never come). A special quorum box
Qr (a) takes quorums of checkpoint messages from servers and (b)immediately passes along recovery messages of servers that havefallen behind. In this way, extension Async2 or refinement RRepS
maintains the abstraction of a single recoverable server RSb .

Async0 extends S (the interface of a non-recoverable server) toRSa (the interface of a recoverable asynchronous server), S RSa .
Recovering from asynchrony includes logging, checkpointing, andthe ability to load a checkpoint and replay the log upon restart.
Most modern request-processing servers implement this functionality, such as Hadoop [25] and Zookeeper [61]. Figure 16 is theinitial PnF architecture of an ACFT server.
C1
RSɲ

C2
...
Cn

Figure 16: Initial ACFT Architecture
C1

5.3

C2
RL
RS
The Async
0 and List Pushoutɴ

Recall that the... List refinement introduces an L box in front of
Cn 6, where L is part of the greater abstraction ofserver S in Figure
one correct server. For the entire abstraction to be recoverable, allof its stateful internal boxes must be recoverable. Async1 modifies the architecture of Figure 6 with two box extensions, L
RL
and RSa
RSb , and adds a new connector: the recoverable list
box needs information from the recoverable server to checkpoint
the server’s state. A “feedback” connector is used to transport thisrequest. The result is Figure 17.

Agreement Replication.

Qr
RSɶ1

C1

C1

RA1

RS

C2

CF2

RA2

RL Qa

...

...

...

...

Cn

Cn

RAn

RSɶn

ɲ

RSɶ2

RSɴ

Qs

5.5

Figure 17: After Extension Async1 or Refinement RList
Qr

F

Admittedly, Figure 17 is evident only to domain experts. To nonRA1 experts, Figure 17 simply statesRSɶthat
1 Qrtherecoverable list and server
1boxes are tightly coupled in Upright’s
design.
Qr
RA2... 5.4

RAn
C1
C2
...
Cn

The Async1 and

RA1

2

RA2

n

RAn

2

Qs

n
Paxos
· RepS... QrPushout

Recalland RepS
refinements
replicateandɶ
C1 the Paxos
F1
RA1RS
Qa1 agreement
RSɶ1kɲ
server boxes. Async2 extends agreement
and serverRSboxes
to supC1
port asynchronousandadds new boxes
andconnectors
toC2 RSɲ
F2 recoveryRAQaRL
RSRSɶ2ɴ
2
2
C2
implementthe“feedback”
connectorofFigure17.
The
result
is
...
...
...
Qr1...
Figure
18.
ɶ
Cn

Fn

Qr2

Qan

RL

RS

RS n

C2

F

...

...

... ɶ

RSɶk

Qsn

10 By receiving occasionally checkpoints from the server, the agree-

RSɶ1

RA2

RSɶ2

Cn

...
RAm

Qak

ɶ

QsRS1 1
RSɶ2

Qa

Qs2

Qs

...

RS k

Qr1
Figure 18: After Extension
Async2 or Refinement RPaxos ·
Qr2
RRepS
Qrn
C1

Qr1

C2

Qr2...

QrnCn
RA1

F1

RA1

F2

RA2

Qa1

RSɶ1

Qs1

Qa2

RSɶ2

Qs2

...
Fn

RAm

Qa1

Validation

We implemented both the SCFT and ACFT architectures by hand,incrementally as described above, using Python 3 atop a custombuilt, light-weight streaming-application framework (code for thiscase study can be downloaded from [21]). Each box was a process;messages were transferred via sockets. We tested the initial archi-

Qa1 RA1
Qa2

The Async2 and Ra · Rb · Rc Pushout
Once again, we are at a point where refinement is inadequate tocomplete the AFCT design; optimizations are needed to complete
the ACFT architecture. The transformation that maps Figure 18 to
Figure 19 is simple: the same optimizations (Ra · Rb · Rc ) that wereused in the SCFT architecture are replayed. Further, the additional
boxes that were added in Figure 18 are all SPoFs. Transformation Rd is a pair of rotations that modify the order (B, Qr, ) to
(B, , Qr) and then to ( , B, Qr). Further, Rd replaces the reliablebroadcast with the normal broadcast •. Doing so removes SPoFs
Qs1 preserves the property that all replica RA boxes receive quorumand
decided messages from server replicas (or “Help!” messages fromQs2
recovering
servers). Optimization Ra · Rb · Rc · Rd of Figure 18, or...
equivalently
extension Async3 of Figure 12, yields Figure 19 (FigureQsn4), Upright’s ACFT server architecture.
5.6

ɴ

Qr

C1

...

Cn

RAn

Qrn

1

RSɶ2

Qa

Extension Async2 maps each agreement box A of Figure 7 toa recoverable agreement box RA, A
RA, that performs the sametasks as an A box, but in addition, responds to new messages, suchas one for receiving the current checkpoint on which the RA replicas
must agree.11 Further, a reliable broadcast ( ) is introduced that
sends all incoming “Help” messages from the server abstraction to
all agreement replicas RA1 . . . RAm . In this way, extension Async2
or refinement RPaxos maintains the behavior of and interface to asingle RL box.

RSɶ1

Qak

...

...

RSɶk

Qsn

Qs1

ment nodes can implement recovery without the requirement of an
infinite replay log. This optimization is obviously desirable.
11 As part of the transformation, the agreement protocol must now
not only agree upon the next client request to transmit, but also on
the checkpoint to save to stable storage.

...

...

...

Cn

RAn

RSk

Qr1
Qr2
Qrn
C1

F1

RA1

Qa1

RS1

Qs1

C2

F2

RA2

Qa2

RS2

Qs2

...
Cn

...
Fn

RAn

Qak

...

...

RSk

Qsn

Figure 19: Asynchronous Crash Fault Tolerant Architecture
tecture and each subsequent architecture that was derived, thereby
validating our transformations.
As future work we hope to collaborate with our ACFT colleagues
to formally prove the correctness of each individual transformation, making this work an example of the correct by construction
paradigm. As mentioned earlier, Clement et al. have a proof of thecomposite transformation for the ACFT architecture [14], but not
proofs for each individual transformation. Although special casesof the ACFT proof reduce to proofs of specific compositions oftransformations, it is unclear whether proofs of individual transformations are ultimately simpler than proofs of a single composite
transformation.
Interestingly, rotations were unfamiliar to our ACFT colleagues.
Their informal designs went directly from Figure 5b to Figure 19,
avoiding our incremental construction of a reliable crossbar. This
discovery suggests how our approach may explain complex andintuitive designs in a structured way.

5.7

EpilogWe continued to elaborate our ACFT design to Upright’s full design for a Byzantine Fault Tolerant (BFT) server. This required
architectural extensions and pushouts to the ACFT architectures(right-hand sides of Figure 15) to add batching, authentication, andmachine boundaries.
In doing so, we saw a pattern that shed light on limitations ofclassical approaches. The first is simple: optimizations are notalways included in refinement methodologies. Optimizations are
essential in Upright’s design.
Second, classical approaches are known to have difficulty scaling [48]. To see this, consider Figure 20. Traditionally, one starts
with a simple architecture A1 and progressively extends it to A2 ,A3 , and A4 before refinements A4 ! B4 , B4 ! C4 , and C4 ! D4 areapplied to derive the final architecture D4 .
We observed that the sequence of extensions that are applied to
an initial architecture are generally easy to understand—there is
Traditional Pathextension

B

A1

A2

A3

A4

B1

B2

B3

B4

C1

C2

C3

C4

D1

D2

D3

D4

E

refinement

AF

pushout

Incremental Path

Figure 20: Paths

little or no detail at this level. (This is the A1 ) · · · ) A4 path). In
contrast, the transformations that are applied to the fully-extended
architecture A4 integrate all of the refinements, optimizations, andextensions that preceded it. For example, refinement B4 ! C4 maps
the result of composite arrow A1 ) B4 to the result of composite
arrow A1 ) C4 . While each individual arrow of a composite canbe grasped by uninitiated readers, monolithic composites are only
understood by domain experts.
This observation has practical significance: had we followed
the classical approach where a specification is fully elaborated before refinement takes place [52], we could not have understood, letalone derived, Upright’s architecture. The required (composite) refinements were simply too complicated to understand and explain.
Pushouts were needed to synthesize complicated architectural designs. Their use allows us to understand how “derivation replay”
is accomplished in the presence of extensions. We now know whatto add and what to change in a derivation.
Stated bluntly, classical approaches without the aid of pushouts
and optimizations cannot describe practical systems.

6.

RELATED WORKThe idea of using pushouts is not new in software development.
Smith [51] used pushouts to automatically compute how to apply
an abstract algebraic specification of an extension to an algebraic
specification of an algorithm. Morphisms model how extensions
are applied to abstract algebraic specifications, and tactics are used
to find possible ways of applying the same extension to concretealgorithms. Smith starts with algebraic specifications, whereas we
use pipe-and-filter architectures.
Amphion is a classic example of Knowledge Base Software Engineering (KBSE) [38]. It provides a DSL to write an abstract FOL
specification (theorem) of the problem to solve. Amphion relies
on a domain theory (a formalization of a domain and its implemented components in a library) and uses deductive synthesis toprove the theorem from which a program is extracted. If a theorem
is changed, Amphion starts its entire process from scratch. This ispossible if one has a rather complete knowledge base. In our case,the set of extensions (features) that can be applied to an architecture is open-ended. And even in the common case where one limits
the set of extensions, there is the problem of how to populate theknowledge base with transformations that can derive extended programs. Pushouts explain how refinements of extended architectures
can be created.
Pipe-and-filter architectures are a fundamental class of software
designs [22]. Practical tools for building PnF architectures havea long history. LabVIEW [44], Weaves [23], and Fractal [10] areplatforms for executing PnF architectures. Other component-based
systems or languages follow a similar approach [22, 32, 54, 58].
Refinement is their sole abstraction; user-defined optimizations, extensions, and pushouts are absent.
Our work is an example of Model Driven Engineering (MDE):
we map high-level models of architectures to low-level models ofarchitectures. We rely on endogenous transformations—transformations whose domain and co-domain are the same. Most of the
MDE literature focuses on exogenous transformations—mappings
whose domain and co-domain are different [40]. For example, eacharchitectural style has its own metamodel. Prior work mapped architectures of one style to an architecture of another [1, 18, 26,56]. Endogenous transformations have been used sparingly, not forincremental architectural development as we do, but to simulate architecture execution (e.g. adding and removing clients in a clientserver system) [11, 41]. The few cases where endogenous transformations are composed to produce MDE designs [55, 57, 62]deal with simple transformations that encode extensions as modeldeltas, not refinements and optimizations that we present.
Banach et al. [4] propose the concept of retrenchment to improve the refinements ability to deal with the complexity of thereal world, or the limitations of models closer to the implementation (e.g. the need to handle error situations). Retrenchment may
be compared to extensions, as both allow to add new behavior tomodels/specifications. However, retrenchment deals with exogenous transformations, adding new behavior to specifications in one
domain to a more concrete domain.
Burstall and Darlington [12] proposed a transformation system
for recursive programs. Their folding and unfolding operations are
similar to our abstraction and refinement transformations. They
used equational rewrites, whereas we are using graph rewrites. Moreover, their approach did not account for extensions or pushouts, thatwere essential to our work.
There is a rich collection of papers on architecture refinement;
we limit our discussions to key papers for lack of space. Traditional approaches start with an abstract architecture or specificationand then apply refinements to progressively expose more hierarchical detail on how the abstract architecture is implemented. Some
researchers have shown that their refinements can be verified, notviolating any of the original design’s properties [7, 26, 41, 42]. Our
work differs from traditional refinement in three ways: 1) We startwith a simple architecture and apply endogenous transformations toextend it and to expose implementation details. 2) We are unawareof prior work that uses architectural optimizations and pushouts inthe development of PnF systems. And 3) the role of extension in
SWD architectural design is under-appreciated. Broy seems to lay
the mathematical foundations for extension [9], but we are unawareof a recent system that puts his ideas into practice.
Our work is an example of software architecture recovery [17,33]. Classic research focuses on tools, data exchange formats,and metrics for extracting and clustering information from source(code, makefiles, documentation, etc.) and application execution
traces to reconstruct an architecture [19, 28, 39]. Our approachis different: our decomposition is based on semantics and not metrics; our source is our understanding of a domain and that which we
can gain from domain-experts, rather than from code and execution
traces. Our work is more in line with architectural recovery using
MDE, where a system is described by multiple viewpoints (metamodels) and their views (models) [19]. But even here our work
is different, as we start with a well-known viewpoint (a pipe-andfilter architecture) and stress the role of transformations to derive
an architecture’s design.
Some of our refinements are similar to algorithmic skeletons [15],in particular the map skeleton [2]. Although some skeleton approaches support optimizations of skeleton compositions [2], they
do not provide support for user-defined optimizations, nor extensions.
Finally, our work may eventually be an example of the correct
by construction paradigm: if the initial architecture is correct, andits transformations are correct, the resulting architecture is correct.
Clement et al. have a proof of the composite transformation for the
ACFT architecture [14], but not proofs for each individual transformation.

7.

CONCLUSIONS

Automated support for program derivation and program evolution is an important objective: it is widely believed that it will yielda major improvement in the software lifecycle [24]. We seek toreveal a process by which architectural designs can be defined byrefinement, optimization, and extension, from which legacy applications can be reconstructed from our models.
In this paper, we explained how we reverse-engineered Upright,
a complex state-of-the-art asynchronous crash fault tolerant (ACFT)
server. We provided strong evidence for the following points: (1)that optimizations and pushouts—in addition to refinement and extension—are essential in software architectural recovery, and (2)that refining fully-specified systems can be difficult or impractical.
We found it easier to refine a simple description of a system througha series of progressively more detailed implementations, and thenextend each of these implementations using pushouts to “replay
derivations” of prior refinements. The value in doing so is that we
now know how to populate a knowledge base of transformations,transformations that can be grasped by uninitiated readers, whilemonolithic composite transformations are only understood by domain experts. To validate our study, we recreated Upright’s ACFT
and SCFT architectures following the derivation that we presented
in this paper.
As of this writing, we are building a domain-independent MDE
tool that aids the process described in this paper, and that supports
refinements, extensions, and optimizations. This paper provides
a foundation to codify domain-specific knowledge in a machinemanipulatable way, which is a necessary foundational step for building semi-automated tools for 1) reverse engineering software architectures from complex, expert-built applications, and 2) recreating
applications using these models.
Acknowledgments: We gratefully acknowledge helpful feedback
from E. Torlak (MIT), G. Heineman (WPI), G. Karsai (Vanderbilt),
E. Hehner (Toronto), H. Vin (Tata Consulting), and A. Clement(Texas). Batory and Riché are supported by the NSF’s Scienceof Design Project CCF 0724979 and NSF’s Computer Systems
Research Grant CNS 0509338. Marker was supported by sponsored by NSF grant CCF-0917167, a fellowship from Sandia National Laboratories, and an NSF Graduate Research Fellowship under grant DGE-1110007. Gonçalves is supported by Portuguese
Science Foundation (FCT) grant SFRH/BD/47800/2008 and FCT
project UTAustin/CA/0056/2008.

8.

REFERENCES[1] M. Abi-Antoun and N. Medvidovic. Enabling the Refinementof a Software Arch. into a Design. In UML, 1999.
[2] M. Aldinucci, M. Coppola, and M. Danalutto. Rewriting
skeleton programs: how to evaluate the data-parallel
stream-parallel tradeoff. In CMPP, 1998.
[3] S. Apel, C. Kästner, and C. Lengauer. Featurehouse:
Language-independent, automated software composition. In
ICSE, 2009.
[4] R. Banach, M. Poppleton, C. Jeske, and S. Stepney.
Engineering and theoretical underpinnings of retrenchment.
Sci. Comput. Program., 67(2-3):301–329, 2007.
[5] D. Batory, J. Sarvela, and A. Rauschmayer. Scaling
Step-Wise Refinement. IEEE TSE, June 2004.
[6] I. D. Baxter. Design Maintenance Systems. CACM, April
1992.
[7] J. P. Bernhard and B. Rumpe. Stepwise Refinement of Data
Flow Architectures. Technical Report TUM-19746, TU
München, 1997.
[8] R. V. Book. Confluent and other types of thue systems. J.
ACM, 29:171–182, January 1982.
[9] M. Broy. Compositional Refinement of Interactive Systems.
JACM, 44(6), 1992.

[10] E. Bruneton, T. Coupaye, and J. Stefani. The Fractal
Component Model. http://fractal.ow2.org, 2004.
[11] R. Bruni, A. Bucchiarone, S. Gnesi, D. Hirsch, and A. L.
Lafuente. Graph-Based Design and Analysis of Dynamic
Software Arch. In LNCS. Springer-Verlag, 2008.
[12] R. Burstall and J. Darlington. A transformation system fordeveloping recursive programs. J. ACM, 24(1):44–67, 1977.
[13] M. Castro. Practical Byzantine Fault Tolerance. PhD thesis,
MIT, Jan. 2001.
[14] A. Clement, M. Kapritsos, S. Lee, Y. Wang, L. Alvisi,
M. Dahlin, and T. L. Riché. UpRight Cluster Services. In
SOSP, Oct. 2009.
[15] M. Cole. Algorithmic skeletons: structured management ofparallel computation. MIT Press, Cambridge, MA, USA,1989.
[16] J. Dean and S. Ghemawat. MapReduce: Simplified Data
Processing on Large Clusters. In OSDI, Dec. 2004.
[17] S. Ducasse, D. Pollet, and L. Poyet. A Process-Oriented
Software Arch. Reconstruction Taxonomy. In CSMR, 2007.
[18] A. Egyed, N. Mehta, and N. Medvidovic. SW Connectors
and Refinement in Family Arch. In IWSAPF, 2000.
[19] J. Favre. Cacophony: Metamodel-driven architecture
recovery. In WCRE, 2004.
[20] M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibilityof Distributed Consensus with One Faulty Process. J. ACM,
32:374–382, April 1985.
[21] Code Generator.
http://code.google.com/p/stepwise-ft/.
[22] D. Garlan. Style-Based Refinement for Software
Architecture. In ISAW, 1996.
[23] M. M. Gorlick and R. R. Razouk. Using Weaves for
Software Construction and Analysis. In ICSE, 1991.
[24] C. Green, D. Luckham, R. Balzer, T. Cheatham, and C. Rich.
Report on a knowledge-based software assistant. KestrelInstitute Technical Report KES.U.83.2, 1983.
[25] Hadoop. http://hadoop.apache.org/core/.
[26] R. Heckel and S. Thöne. Behavior-Preserving Refinement
Relations Between Dynamic Soft. Arch. In WADT, 2004.
[27] E. Hehner. Predicative Programming Part 1. CACM, 1984.
[28] R. Holt, A. Winter, and A. Schurr. GXL: Toward a Standard
Exchange Format. In Reverse Engineering, Nov. 2000.
[29] K. Kang, S. Cohen, J. Hess, W. Novak, and A. Peterson.
Feature-oriented domain analysis (foda) feasibility study.
CMU/SEI-90-TR-021, 1990.
[30] I. Kassios. A Theory of Object Oriented Refinement. PhD
thesis, University of Toronto, 2006.
[31] C. Kästner, S. Apel, and M. Kuhlemann. Granularity insoftware product lines. In ICSE, 2008.
[32] E. Kohler, R. Morris, B. Chen, J. Jannotti, and M. F.
Kaashoek. The Click Modular Router. ACM Trans. Comput.
Syst., 18(3):263–297, Aug. 2000.
[33] R. Koschke. Architecture Reconstruction: Tutorial on
Reverse Engineering to the Architectural Level. In LNCS
5413, 2009.
[34] R. Kotla. xbft: Bzyantine Fault Tolerance with High
Performance, Low Cost, and Aggressive Fault Isolation. PhD
thesis, The University of Texas at Austin, 2008.
[35] R. Kotla, L. Alvisi, M. Dahlin, A. Clement, and E. Wong.
Zyzzyva: Speculative Byzantine Fault Tolerance. In SOSP,
Oct. 2007.
[36] L. Lamport. The Part-Time Parliament. ACM ToCS,

16(2):133–169, 1998.
[37] H. C. Li, A. Clement, A. S. Aiyer, and L. Alvisi. The Paxos
Register. In IEEE SRDS, 2007.
[38] M. R. Lowry, A. Philpot, T. Pressburger, and I. Underwood.
Amphion: Automatic programming for scientific subroutine
libraries. In ISMIS, 1994.
[39] O. Maqbool and H. Babri. Hierarchical Clustering for
Software Arch. Recovery. IEEE TSE, pages 759–780, 2007.
[40] T. Mens and et al. A Taxonomy of Model Transformations.
In GraMoT, 2005.
[41] D. L. Métayer. Describing Software Arch. Styles Using
Graph Grammars. IEEE TSE, 24(7):521–533, 1998.
[42] M. Moriconi, X. Qian, and R. A. Riemenschneider. Correct
Architectural Refinement. IEEE TSE, 21:356–372, 1995.
[43] S. Mullender, editor. Distributed Systems. Addision-Wesley,
2nd edition, 2003.
[44] National Instruments LabVIEW 2011.
http://www.ni.com/labview/.
[45] Future of Software Engineering Research.
http://www.nitrd.gov/SUBCOMMITTEE%5Csdp%5Cfoser%
5CFOSER%20December%202011.pdf, 2011.
[46] C. H. Papadimitriou. The Serializability of Concurrent
Database Updates. J. ACM, 26(4):631–653, 1979.
[47] B. Pierce. Basic Category Theory for Computer Scientists.
MIT Press, 1991.
[48] M. Poppleton. Private Correspondence. Private
Correspondence, 2010.
[49] F. B. Schneider. Implementing Fault-Tolerant Services Using
the State Machine Approach: A Tutorial. ACM Computing
Surveys, 22(4):299–319, Sept. 1990.
[50] M. Shaw and D. Garlan. Software Architecture: Perspectives
on an Emerging Discipline. Prentice Hall, 1996.
[51] D. Smith. Mechanizing the development of software. In
Proc. of the Marktoberdorf Int. Summer School, 1999.
[52] J. Spivey. The Z Notation: A Reference Manual. Prentice
Hall, 1989.
[53] J. M. Spivey. The Z Notation: A Reference Manual, 1998.
[54] W. Thies. Lang. and Compiler Support for Stream Programs.
PhD thesis, MIT, Feb. 2009.
[55] S. Trujillo, D. Batory, and O. Diaz. Feature Oriented Model
Driven Develop.: A Case Study for Portlets. In ICSE, 2007.
[56] T. Tseng, J. Aldrich, D. Garlan, and B. Schmerl. Semantic
Issues in Arch. Refinement. Technical report, CMU, 2004.
[57] M. Volter and I. Groher. Product Line Implementation using
AO and MD Software Development. In SPLC, 2007.
[58] S. Wang, G. S. Avrunin, and L. A. Clarke. Arch. Building
Blocks for Plug-and-Play System Design. In CBSE, 2006.
[59] N. Wirth. Program Development by Stepwise Refinement.
CACM, 1971.
[60] J. Yin, J.-P. Martin, A. Venkataramani, L. Alvisi, and
M. Dahlin. Separating Agreement from Execution for
Byzantine Fault Tolerant Servers. In SOSP, 2003.
[61] Zookeeper. http://hadoop.apache.org/zookeeper.
[62] S. Zschaler and et. al. VML*: A Family of Languages for
Variability Management in Software Product Lines. In SLE,2009.