% Please keep this file in TR Number order (reverse chronological order)
% Please follow the TR key format "LastNamesOfAllAuthors:bucs-YYYY-NNN"

@techreport{BUCS-TR-2006-029,
   author = {Likai Liu and Assaf Kfoury},
   title = {{Safe Compositional Specification of Network Systems With Polymorphic, Constrained Types}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-029},
   month = {{October 25}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-029-poly-constrained-traffic.pdf},
   abstract = {
In the framework of iBench research project, our previous work created
a domain specific language TRAFFIC [BUCS-TR-2005-015] that facilitates
specification, programming, and maintenance of distributed
applications over a network. It allows safety property to be
formalized in terms of types and subtyping relations. Extending upon
our previous work, we add Hindley-Milner style polymorphism
[Milner:JCSS-1978-v17] with constraints [Odersky:TPOS-1999-v5] to the
type system of TRAFFIC. This allows a programmer to use for-all
quantifier to describe types of network components, escalating power
and expressiveness of types to a new level that was not possible
before with propositional subtyping relations. Furthermore, we design
our type system with a pluggable constraint system, so it can adapt to
different application needs while maintaining soundness.
  In this paper, we show the soundness of the type system, which is not 
syntax-directed but is easier to do typing derivation. We show that 
there is an equivalent syntax-directed type system, which is what a 
type checker program would implement to verify the safety of a network 
flow. This is followed by discussion on several constraint systems: 
polymorphism with subtyping constraints, Linear Programming, and 
Constraint Handling Rules (CHR) [Fruhwirth:JLP-1998-v37]. Finally, we 
provide some examples to illustrate workings of these constraint 
systems.}
}

@techreport{BUCS-TR-2006-016,
   author = {Michael Ocean and Assaf Kfoury and Azer Bestavros},
   title = {{Integrating Sensor-Network Research and Development into a Software Engineering Curriculum}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-016},
   month = {{July 14}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-016-snbench-cs511-curriculum.pdf},
   abstract = {
The emergence of a sensor-networked world produces a clear and urgent
need for well-planned, safe and secure software engineering.  It is the 
role of universities to prepare graduates with the knowledge and 
experience to enter the work-force with a clear understanding of 
software design and its application to the future safety of computing. 
The snBench (Sensor Network WorkBench) project aims to provide support 
to the programming and deployment of Sensor Network Applications, 
enabling shared sensor embedded spaces to be easily tasked with
various sensory applications by different users for simultaneous 
execution.  In this report we discus our experience using the snBench 
research project as the foundation for semester-long project in a 
graduate level software engineering class at Boston University (CS511).}
}


@techreport{BUCS-TR-2006-015,
   author = {Dustin Burke and Dave Cecere and Ben Freiberg},
   title = {{Extending snBench to Support a Video-Based Intrusion Detection and Alerting System with a Centralized Hash Table}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-015},
   month = {{July 14}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-015-snbench-centralized-hash.pdf},
   abstract = {
In this project we design and implement a centralized hashing table
in the snBench sensor network environment.  We discuss the feasibility 
of this approach and compare and contrast with the distributed hashing 
architecture, with particular discussion regarding the conditions under 
which a centralized architecture makes sense.
There are numerous computational tasks that require persistence of data 
in a sensor network environment.  To help motivate the need for data 
storage in snBench we demonstrate a practical application of the 
technology whereby a video camera can monitor a room to detect the 
presence of a person and send an alert to the appropriate authorities.}
}

@techreport{BUCS-TR-2006-014,
   author = {Ching Chang and Raymond Sweha and Panagiotis Papapetrou},
   title = {{Extending snBench to Support a Graphical Programming Interface for a Sensor Network Tasking Language ({STEP})}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-014},
   month = {{July 14}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-014-snBench-programming-gui.pdf},
   abstract = {
We report on our development and implementation of a graphical 
"programming" interface for a sensor network tasking language called 
STEP. The graphical interface allows the user to specify a program 
execution graphically from an extensible pallet of functionalities and 
save the results as a properly formatted STEP file. Moreover, the 
software is able to load a file in STEP format and convert it into the 
corresponding graphical representation. During both phases a 
type-checker is running on the background to ensure that both the 
graphical representation and the STEP file are syntactically correct. 
This project has been motivated by the Sensorium project at Boston 
University. In this technical report we present the basic features of 
the software, the process that has been followed during the design and 
implementation. Finally, we describe the approach used to test and 
validate our software.}
}

@techreport{BUCS-TR-2006-013,
   author = {Jorge Londono and Sowmya Manjanatha and Zhinan Han},
   title = {{Extending snBench to Provide Concurrency Support in the Sensorium Execution Environment ({SXE})}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-013},
   month = {{July 14}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-013-snBench-sxe-concurrency.pdf},
   abstract = {
The SNBENCH is a general-purpose programming environment and run-time 
system targeted towards a variety of Sensor applications such as 
environmental sensing, location sensing, video sensing, etc. In its 
current structure, the run-time engine of the SNBENCH namely, the 
Sensorium Execution Environment (SXE) processes the entities of 
execution in a single thread of operation. In order to effectively 
support applications that are time-sensitive and need priority, it is 
imperative to process the tasks discretely so that specific policies can 
be applied at a much granular level. The goal of this project was to 
modify the SXE to enable efficient use of system resources by way
of multi-tasking the individual components. Additionally, the 
transformed SXE offers the ability to classify and employ different 
schemes of processing to the individual tasks.}
}

@techreport{BUCS-TR-2006-012,
   author = {Gabriel Parmer and Georgios Zervas and Angshuman Bagchi},
   title = {{Extending snBench to Support Hierarchical and Configurable Scheduling}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-012},
   month = {{July 14}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-012-snBench-hierarchical-scheduling.pdf},
   abstract = {
It is useful in systems that must support multiple applications with
various temporal requirements to allow application-specific policies to
manage resources accordingly.  However, there is a tension between this
goal and the desire to control and police possibly malicious programs.
The Java-based Sensor Execution Environment (SXE) in snBench presents a
situation where such considerations add value to the system.  Multiple
applications can be run by multiple users with varied temporal
requirements, some Real-Time and others best effort. This paper
outlines and documents an implementation of a hierarchical  
and configurable scheduling system with which different applications can 
be executed using application-specific scheduling policies. Concurrently 
the system administrator can define fairness policies between 
applications that are imposed upon the system.  Additionally, to ensure 
forward progress of system execution in the face of malicious or 
malformed user programs, an infrastructure for execution using multiple 
threads is described.}
}

@techreport{BUCS-TR-2006-001,
   author = {Yarom Gabay and Michael Ocean and Assaf Kfoury and Likai Liu},
   title = {{Computational Properties of {SNAFU}}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2006-001},
   month = {{February 6}},
   year = {2006},
   url = {http://www.cs.bu.edu/techreports/pdf/2006-001-snafu-properties.pdf},
   abstract = {
Sensor applications in Sensoria
\cite{BestavrosBradleyKfouryOcean:basenets05} are expressed using STEP
($\backslash$mph{Sensorium Task Execution Plan}). SNAFU ($\backslash$mph{SensorNet
Applications as Functional Units}) serves as a high-level
sensor-programming language, which is compiled into STEP. In SNAFU's
current form, its differences with STEP are relatively minor, as they
are limited to shorthands and macros not available in STEP. We show
that, however restrictive it may seem, SNAFU has in fact universal
power; technically, it is a Turing-complete language, i.e., any Turing
program can be written in SNAFU (though not always conveniently).
Although STEP may be allowed to have universal power, as a low-level
language not directly available to Sensorium users, SNAFU programmers
may use this power for malicious purposes or inadvertently introduce
errors with destructive consequences. In future developments of SNAFU,
we plan to introduce restrictions and high-level features with safety
guards, such as those provided by a type system, which will make SNAFU
programming safer.}
}


@techreport{BUCS-TR-2005-034,
   author = {Yarom Gabay and Assaf Kfoury and Likai Liu and Azer Bestavros and Adam Bradley and Ibrahim Matta},
   title = {{Type Systems for a Network Specification Language With Multiple-Choice Let}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2005-034},
   month = {{December 28}},
   year = {2005},
   url = {http://www.cs.bu.edu/techreports/pdf/2005-034-traffic-multiple-let-binding.pdf},
   abstract = {
When analysing the behavior of complex networked systems, it is often
the case that some components within that network are only 
known to the extent that they belong to one of a set of possible
"implementations" -- e.g., versions of a specific protocol, class of
schedulers, etc.  In this report we augment the specification language
considered in BUCS-TR-2004-021, BUCS-TR-2005-014, BUCS-TR-2005-015,
and BUCS-TR-2005-033, to include a non-deterministic multiple-choice
let-binding, which allows us to consider compositions of networking
subsystems that allow for looser component specifications.}
}

@techreport{BUCS-TR-2005-033,
   author = {Likai Liu and Assaf Kfoury and Azer Bestavros and Yarom Gabay and Adam Bradley and Ibrahim Matta},
   title = {{Safe Compositional Specification of Networking Systems: {A} Compositional Analysis Approach}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2005-033},
   month = {{December 28}},
   year = {2005},
   url = {http://www.cs.bu.edu/techreports/pdf/2005-033-traffic-compositional-analysis.pdf},
   abstract = {
We present a type inference algorithm, in the style of compositional
analysis, for the language TRAFFIC---a specification language for flow
composition applications proposed in BUCS-TR-2005-014---and prove that
this algorithm is correct: the typings it infers are principal
typings, and the typings agree with syntax-directed type checking on
closed flow specifications. This algorithm is capable of verifying
partial flow specifications, which is a significant improvement over
syntax-directed type checking algorithm presented in BUCS-TR-2005-015.
We also show that this algorithm runs efficiently, i.e., in low-degree
polynomial time.}
}

@techreport{BUCS-TR-2005-014,
   author = {Azer Bestavros and Adam Bradley and Assaf Kfoury and Ibrahim Matta},
   title = {{Typed Abstraction of Complex Network Compositions}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2005-014},
   month = {{May 1}},
   year = {2005},
   url = {http://www.cs.bu.edu/techreports/pdf/2005-014-traffic-framework.pdf},
   abstract = {
The heterogeneity and open nature of network systems make analysis of
compositions of components quite challenging, making the design and
implementation of robust network services largely inaccessible to the
average programmer.  We propose the development of a novel type system
and practical type spaces which reflect simplified representations of
the results and conclusions which can be derived from complex
compositional theories in more accessible ways, essentially allowing
the system architect or programmer to be exposed only to the inputs
and output of compositional analysis without having to be familiar
with the ins and outs of its internals.  Toward this end we present
the TRAFFIC (Typed Representation and Analysis of Flows For
Interoperability Checks) framework, a simple flow-composition and
typing language with corresponding type system.  We then discuss and
demonstrate the expressive power of a type space for TRAFFIC derived
from the network calculus, allowing us to reason about and infer such
properties as data arrival, transit, and loss rates in large composite
network applications.}
}

@techreport{BUCS-TR-2005-015,
   author = {Likai Liu and Assaf Kfoury and Azer Bestavros and Adam Bradley and Yarom Gabay and Ibrahim Matta},
   title = {{Safe Compositional Specification of Networking Systems: {TRAFFIC} The Language and Its Type Checking}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2005-015},
   month = {{May 12}},
   year = {2005},
   url = {http://www.cs.bu.edu/techreports/pdf/2005-015-traffic-types.pdf},
   abstract = {
This paper formally defines the operational semantic for TRAFFIC, a
specification language for flow composition applications proposed in
BUCS-TR-2005-014, and presents a type system based on desired
safety assurance. We provide proofs on reduction (weak-confluence,
strong-normalization and unique normal form), on soundness and
completeness of type system with respect to reduction, and on
equivalence classes of flow specifications. Finally, we provide a
pseudo-code listing of a syntax-directed type checking algorithm
implementing rules of the type system capable of inferring the type of
a closed flow specification.}
}

@techreport{BUCS-TR-2004-021,
   author = {Azer Bestavros and Adam Bradley and Assaf Kfoury and Ibrahim Matta},
   title = {{Safe Compositional Specification of Networking Systems}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2004-021},
   month = {{May 14}},
   year = {2004},
   url = {http://www.cs.bu.edu/techreports/pdf/2004-021-compositional-net-specs.pdf},
   abstract = {
The Science of Network Service Composition has clearly emerged as one
of the grand themes driving many of our research questions in the
networking field today [NeXtworking 2003]. This driving force stems
from the rise of sophisticated applications and new networking
paradigms.  By ``service composition'' we mean that the performance
and correctness properties local to the various constituent components
of a service can be readily composed into global (end-to-end)
properties without re-analyzing any of the constituent components in
isolation, or as part of the whole composite service.  The set of laws
that would govern such composition is what will constitute that new
science of composition. 
  The combined heterogeneity and dynamic open nature of network
systems makes composition quite challenging, and thus programming
network services has been largely inaccessible to the average user.
We identify (and outline) a research agenda in which we aim to develop
a specification language that is expressive enough to describe
different components of a network service, and that will include type
hierarchies inspired by type systems in general programming languages
that enable the safe composition of software components.  We envision
this new science of composition to be built upon several theories
(e.g., control theory, game theory, network calculus, percolation
theory, economics, queuing theory). In essence, different theories may
provide different languages by which certain properties of system
components can be expressed and composed into larger systems.  We then
seek to lift these lower-level specifications to a higher level by
abstracting away details that are irrelevant for safe composition at
the higher level, thus making theories scalable and useful to the
average user.
  In this paper we focus on services built upon an overlay management 
architecture, and we use control theory and QoS theory as example
theories from which we lift up compositional specifications.}
}

@techreport{BUCS-TR-2004-007,
   author = {Adam Bradley and Assaf Kfoury and Azer Bestavros},
   title = {{StaXML: Static Typing of {XML} Document Fragments for Imperative Web Scripting Languages}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2004-007},
   month = {{February 13}},
   year = {2005},
   url = {http://www.cs.bu.edu/techreports/pdf/2004-007-staxml.pdf},
   abstract = {
We present a type system, StaXML, which employs the stacked type syntax
to represent essential aspects of the potential roles of XML fragments
to the structure of complete XML documents. The simplest application of
this system is to enforce well-formedness upon the construction of XML
documents without requiring the use of templates or balanced "gap
plugging" operators; this allows it to be applied to programs written
according to common imperative web scripting idioms, particularly the
echoing of unbalanced XML fragments to an output buffer.  The system can
be extended to verify particular XML applications such as XHTML and
identifying individual XML tags constructed from their lexical
components. We also present StaXML for PHP, a prototype precompiler for
the PHP4 scripting language which infers StaXML types for expressions
without assistance from the programmer.}
}

@techreport{BUCS-TR-2003-032,
   author = {Gali Diamant and Leonid Veytser and Ibrahim Matta and Azer Bestavros and Mina Guirguis and Liang Guo and Yuting Zhang and Sean Chen},
   title = {{itmBench: Generalized {API} for Internet Traffic Managers}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2003-032},
   month = {{December 16}},
   year = {2003},
   url = {http://www.cs.bu.edu/techreports/pdf/2003-032-itmbench.pdf},
   abstract = {
Internet Traffic Managers (ITMs) are special machines placed at
strategic places in the Internet. itmBench is an interface that allows
users (e.g. network managers, service providers, or experimental
researchers) to register different traffic control functionalities to
run on one ITM or an overlay of ITMs.  Thus itmBench offers a
tool that is extensible and powerful yet easy to maintain.  ITM
traffic control applications could be developed either using a kernel
API so they run in kernel space, or using a user-space API so they run
in user space.  We demonstrate the flexibility of itmBench by
showing the implementation of both a kernel module that provides a
differentiated network service, and a user-space module that provides
an overlay routing service. Our itmBench Linux-based prototype is free
software and can be obtained from http://www.cs.bu.edu/groups/itm/.}
}

@techreport{BUCS-TR-2003-012,
   author = {Adam Bradley and Azer Bestavros and Assaf Kfoury},
   title = {{Systematic Verification of Safety Properties of Arbitrary Network Protocol Compositions Using {CHAIN}}},
   institution = {CS Department, Boston University},
   number = {BUCS-TR-2003-012},
   month = {{May 16}},
   year = {2003},
   url = {http://www.cs.bu.edu/techreports/pdf/2003-012-chain-safety-verification.pdf},
   abstract = {
Formal correctness of complex multi-party network protocols can be
difficult to verify. While models of specific fixed compositions of agents
can be checked against design constraints, protocols which lend themselves
to arbitrarily many compositions of agents--such as the chaining of
proxies or the peering of routers--are more difficult to verify because
they represent potentially infinite state spaces and may exhibit emergent
behaviors which may not materialize under particular fixed compositions.
We address this challenge by developing an algebraic approach that enables
us to reduce arbitrary compositions of network agents into a
behaviorally-equivalent (with respect to some correctness property)
compact, canonical representation, which is amenable to mechanical
verification. Our approach consists of an algebra and a set of
property-preserving rewrite rules for the Canonical Homomorphic
Abstraction of Infinite Network protocol compositions (CHAIN). Using
CHAIN, an expression over our algebra (i.e., a set of configurations of
network protocol agents) can be reduced to another behaviorally-equivalent
expression (i.e., a smaller set of configurations). Repeated applications
of such rewrite rules produces a canonical expression which can be checked
mechanically. We demonstrate our approach by characterizing deadlock-prone
configurations of HTTP agents, as well as establishing useful properties
of an overlay protocol for scheduling MPEG frames, and of a protocol for
Web intra-cache consistency.}
}

@techreport{BradleyBestavrosKfoury:bucs-2002-030, 
   author={Adam Bradley and Azer Bestavros and Assaf Kfoury}, 
   title={{Validating Arbitrarily Large Network Protocol Compositions with Finite Computation}},
   institution={Boston University, Computer Science Department}, 
   number={BUCS-TR-2002-030},
   month={November}, 
   year=2002,
   url={http://www.cs.bu.edu/techreports/pdf/2002-030-finite-net-protocol-compositions.pdf},
   keywords={Web Caching, Internet Protocols, Formal verification, HTTP, Interoperability, Model checking, Protocol composition},
   abstract={Formal tools like finite-state model checkers have proven
     useful in verifying the correctness of systems of bounded size
     and for hardening single system components against arbitrary
     inputs.  However, conventional applications of these techniques
     are not well suited to characterizing emergent behaviors of large
     compositions of processes.  In this paper, we present a
     methodology by which arbitrarily large compositions of components
     can, if sufficient conditions are proven concerning properties of
     small compositions, be modeled and completely verified by
     performing formal verifications upon only a finite set of
     compositions.  The sufficient conditions take the form of
     reductions, which are claims that particular sequences of
     components will be causally indistinguishable from other shorter
     sequences of components.  We show how this methodology can be
     applied to a variety of network protocol applications, including
     two features of the HTTP protocol, a simple active networking
     applet, and a proposed web cache consistency algorithm.  We also
     doing discuss its applicability to framing protocol design goals
     and to representing systems which employ non-model-checking
     verification methodologies.  Finally, we briefly discuss how we
     hope to broaden this methodology to more general topological
     compositions of network applications.}
}

@techreport{BradleyBestavrosKfoury:bucs-2002-017,
   author={Adam Bradley and Azer Bestavros and Assaf Kfoury}, 
   title={{Safe Composition of Web Communication Protocols for Extensible Edge Services}},
   institution={Boston University, Computer Science Department}, 
   keywords={Web Caching, Internet Protocols, Formal verification, HTTP, Interoperability, Model checking, Protocol composition},
   number={BUCS-TR-2002-017},
   month={May}, 
   year=2002,
   url={http://www.cs.bu.edu/techreports/pdf/2002-017-http-safe-compositions.pdf},
   abstract={As new multi-party edge services are deployed on the
     Internet, application-layer protocols with complex communication
     models and event dependencies are increasingly being specified
     and adopted. To ensure that such protocols (and compositions
     thereof with existing protocols) do not result in undesirable
     behaviors (e.g., livelocks) there needs to be a methodology for
     the automated checking of the ``safety'' of these protocols. In
     this paper, we present ingredients of such a
     methodology. Specifically, we show how SPIN, a tool from the
     formal systems verification community, can be used to quickly
     identify problematic behaviors of application-layer protocols
     with non-trivial communication models---such as HTTP with the
     addition of the ``100 Continue'' mechanism.  As a case study, we
     examine several versions of the specification for the Continue
     mechanism; our experiments mechanically uncovered multi-version
     interoperability problems, including some which motivated
     revisions of HTTP/1.1 and some which persist even with the
     current version of the protocol.  One such problem resembles a
     classic degradation-of-service attack, but can arise between
     well-meaning peers.  We also discuss how the methods we employ
     can be used to make explicit the requirements for hardening a
     protocol's implementation against potentially malicious peers,
     and for verifying an implementation's interoperability with the
     full range of allowable peer behaviors.}
}

@techreport{BradleyBestavros:bucs-2001-024,
   author={Adam Bradley and Azer Bestavros}, 
   title={{Basis Token Consistency: A Practical Mechanism for Strong Web Cache Consistency}}, 
   institution={Boston University, Computer Science Department}, 
   number={BUCS-TR-2001-024},
   month={October}, 
   year=2001,
   url={http://www.cs.bu.edu/techreports/pdf/2001-024-btc.pdf},
   keywords={Internet, Characterization, Streaming Media, Multicast, Web, Real-Rime},
   abstract={With web caching and cache-related services like CDNs and
     edge services playing an increasingly significant role in the
     modern internet, the problem of the weak consistency and
     coherence provisions in current web protocols is becoming
     increasingly significant and drawing the attention of the
     standards community.  Toward this end, we present
     definitions of consistency and coherence for web-like
     environments, that is, distributed client-server information
     systems where the semantics of interactions with resources are
     more general than the read/write operations found in memory
     hierarchies and distributed file systems.  We then present a
     brief review of proposed mechanisms which strengthen the
     consistency of caches in the web, focusing upon their conceptual
     contributions and their weaknesses in real-world practice.  These
     insights motivate a new mechanism, which we call ``Basis Token
     Consistency'' or BTC; when implemented at the server, this
     mechanism allows any client (independent of the presence and
     conformity of any intermediaries) to maintain a self-consistent
     view of the server's state.  This is accomplished by annotating
     responses with additional per-resource application information
     which allows client caches to recognize the obsolescence of
     currently cached entities and identify responses from other
     caches which are already stale in light of what has already been
     seen.  The mechanism requires no deviation from the existing
     client-server communication model, and does not require servers
     to maintain any additional per-client state.  We discuss how our
     mechanism could be integrated into a fragment-assembling Content
     Management System (CMS), and present a simulation-driven
     performance comparison between the BTC algorithm and the use of
     the Time-To-Live (TTL) heuristic.}  
}