Search

This paper ascribes a formal semantics to advice weaving in AspectJ. Since the version 1.1, AspectJ language is developed using bytecode weaving, which combines aspects and classes to produce ".class" files that run in a Java Virtual Machine (JVM). In AspectJ, advice weaving is done statically by inserting the advice functionality in some regions of the code. These regions are join points that are declared using pointcuts. In this paper, we focus only on static pointcuts, i.e., pointcuts that correspond directly to locations in the bytecode. AspectJ dynamic pointcuts such as target, this, and cflow are not in the focus of this paper. [ABSTRACT FROM AUTHOR]

The static determination of approximated values of string expressions has many potential applications. For instance, approximated string values may be used to check the validity and security of generated strings, as well as to collect the useful string properties. Previous string analysis efforts have been focused primarily on the maxmization of the precision of regular approximations of strings. These methods have not been completely satisfactory due to the difficulties in dealing with heap variables and context sensitivity. In this paper, we present an abstract-interpretation-based solution that employs a heuristic widening method. The presented solution is implemented and compared to JSA. In most cases, our solution gives results as precise as those produced by previous methods, and it makes the additional contribution of easily dealing with heap variables and context sensitivity in a very natural way. We anticipate the employment of our method in practical applications. [ABSTRACT FROM AUTHOR]

This paper tackles a problem often overlooked in functional programming community: that of testing. Fully automatic test tools like ${\sf{Quickcheck}}$ and ${\sf {G{\forall}ST}}$ can test first order functions successfully. Higher order functions, HOFs, are an essential and distinguishing part of functional languages. Testing HOFs automatically is still troublesome since it requires the generation of functions as test argument for the HOF to be tested. Also the functions that are the result of the higher order function needs to be identified. If a counter example is found, the generated and resulting functions should be printed, but that is impossible in most functional programming languages. Yet, bugs in HOFs do occur and are usually more subtle due to the high abstraction level. In this paper we present an effective and efficient technique to test higher order functions by using intermediate data types. Such a data type mimics and controls the structure of the function to be generated. A simple additional function transforms this data structure to the function needed. We use a continuation based parser library as main example of the tests. Our automatic testing method for HOFs reveals errors in the library that was used for a couple of years without problems. [ABSTRACT FROM AUTHOR]

This paper provides a call-by-name and a call-by-value calculus, both of which have a Curry-Howard correspondence to the minimal normal logic K. The calculi are extensions of the λμ-calculi, and their semantics are given by CPS transformations into a calculus corresponding to the intuitionistic fragment of K. The duality between call-by-name and call-by-value with modalities is investigated in our calculi. [ABSTRACT FROM AUTHOR]

This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations. [ABSTRACT FROM AUTHOR]

A natural way to generate test cases for a Prolog program is to view the call patterns of the procedures in the program as an implicit representation of the control flow graph (CFG) of the program. This paper explores the idea by proposing a call patterns-based test case generation method, where a set of call patterns or computed answers is used to describe the paths in a CFG. With a constraint-based call patterns semantics, this method is formalized. Through the use of a proper constraints solver, we can generate test cases automatically from the sets of constraints. This method can be based on any approximation of the call patterns semantics. So compared with traditional CFG-based test case generation, the method is more flexible and can be easily adapted to meet the requirements of a tester expressed by the approximation of the call patterns semantics we use. [ABSTRACT FROM AUTHOR]

Earlier work explored the introduction of session types into object oriented languages. Following the session types literature, two parties would start communicating, provided the types attached to that communication, i.e. the corresponding session types, were dual of each other. Then, the type system was able to ensure soundness, in the sense that two communicating partners were guaranteed to receive/send sequences of values following the order specified by their session types. In the current paper we improve upon our earlier work in two ways: we extend the type system to support bounded polymorphism, and we make the selection more object-oriented, so that control structures determine how to continue evaluation, depending on the class of the object being sent/received. Interestingly, although our notion of selection is more powerful than that in earlier work, the ensuing system turned out not to be more complex, except for the notion of duality, which needed to be extended, to correctly deal with bounded polymorphism, and to capture the new notion of selection. The paper contains an example, informal explanations, a formal description of the operational semantics and of type system, and a proof of subject reduction. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of off-line selection of test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. Efficient solutions to this problem have been proposed in the context of finite-state models, based on the ioco conformance testing theory. An extension of these is proposed in the context of infinite-state specifications, modelled as automata extended with variables. One considers the selection of test cases according to test purposes describing abstract scenarios that one wants to test. The selection of program test cases then consists in syntactical transformations of the specification model, using approximate analyses. [ABSTRACT FROM AUTHOR]

Data centers are the most critical infrastructure of companies demanding higher and higher levels of quality of service (QoS) in terms of availability and scalability. At the core of data centers are multi-tier architectures providing service to applications. Replication is heavily used in this infrastructure for either availability or scalability but typically not for both combined. Additionally, most approaches replicate a single tier, making the non-replicated tiers potential bottlenecks and single points of failure. In this paper, we present a novel approach that provides both availability and scalability for multi-tier applications. The approach uses a replicated cache that takes into account both the application server tier (middle-tier) and the database (back-end). The underlying replicated cache protocol fully embeds the replication logic in the application server. The protocol exhibits good scalability as shown by our evaluation based on the new industrial benchmark for J2EE multi-tier systems, SPECjAppServer. [ABSTRACT FROM AUTHOR]

In this paper we describe an approach in creating private network overlays in user-space to support the dynamic creation of personal clusters on-demand. These personal clusters are created by submitting job proxies to High Performance Computing (HPC) clusters. Job proxies contribute CPU resources back to the personal cluster when they eventually run, allowing application jobs to execute on them in a system call virtualized run-time environment. The virtualized run-time environment enables additional personal cluster-wide services to be interposed, including a private network overlay instantiated for each personal cluster created. The interposed private network overlay allows the personal clusters to tunnel IP traffic thorough gateway nodes at each contributing HPC cluster site in order to provision resources across private networks, survive transient network outages, support critical services like distributed filesystems, and in some cases, improve network transfer throughput across the wide-area network. This paper describes our design and implementation strategy, and concludes with some general guiding principles to aid other projects of a similar nature. [ABSTRACT FROM AUTHOR]

This paper presents the design and implementation of XenSocket, a UNIX-domain-socket-like construct for high-throughput interdomain (VM-to-VM) communication on the same system. The design of XenSocket replaces the Xen page-flipping mechanism with a static circular memory buffer shared between two domains, wherein information is written by one domain and read asynchronously by the other domain. XenSocket draws on best-practice work in this field and avoids incurring the overhead of multiple hypercalls and memory page table updates by aggregating what were previously multiple operations on multiple network packets into one or more large operations on the shared buffer. While the reference implementation (and name) of XenSocket is written against the Xen virtual machine monitor, the principle behind XenSocket applies broadly across the field of virtual machines. [ABSTRACT FROM AUTHOR]

Mobile Ad Hoc Networks (MANETs) offer a flexible way to connect mobile devices to build complex infrastructures. A key issue in MANETs is session set up and management since, unlike in conventional networks, there is no centralized component to provide such a service. Yet, session set up is necessary to provide any form of communication beyond unreliable, single message communication. In this paper we describe SIPHoc, a middleware infrastructure for session set up and management in MANETs. SIPHoc provides the same interface as the SIP standard but its implementation is fully decentralized. Moreover, SIP session establishment to and from the Internet is possible as soon as a single node in the MANET has Internet access. The paper presents the architecture and implementation of SIPHoc and evaluates its performance. The experiments show that SIPHoc is message efficient and provides a low dial-to-ring delay. SIPHoc allows SIP based applications to be used in MANETs without modification. In the paper, this is demonstrated by showing how SIPHoc supports VoIP conversations within a MANET and between the MANET and end-points on the Internet. [ABSTRACT FROM AUTHOR]

In this paper we take advantage of the concepts developed for centralized module management, such as dynamic loading and unloading of modules, and show how they can be used to support the development and deployment of distributed applications. We do so through R-OSGi, a distributed middleware platform that extends the centralized, industry-standard OSGi specification to support distributed module management. To the developer, R-OSGi looks like a conventional module management tool. However, at deployment time, R-OSGi can be used to turn the application into a distributed application by simply indicating where the different modules should be deployed. At run time, R-OSGi represents distributed failures as module insertion and withdrawal operations so that the logic to deal with failures is the same as that employed to deal with dependencies among software modules. In doing so, R-OSGi greatly simplifies the development of distributed applications with no performance cost. In the paper we describe R-OSGi and several use cases. We also show with extensive experiments that R-OSGi has a performance comparable or better than that of RMI or UPnP, both commonly used distribution mechanisms with far less functionality than R-OSGi. [ABSTRACT FROM AUTHOR]

Many state-based specification languages, including the Java Modeling Language (JML), contain at their core specification constructs familiar to most undergraduates: e.g., assertions, pre- and postconditions, and invariants. Unfortunately, these constructs are not sufficiently expressive to permit formal modular verification of programs written in modern object-oriented languages like Java. The necessary extra constructs for specifying an object-oriented module include (perhaps the less familiar) frame properties, datagroups, and ghost and model fields. These constructs help specifiers deal with potential problems related to, for example, unexpected side effects, aliasing, class invariants, inheritance, and lack of information hiding. This tutorial paper focuses on JML's realization of these constructs, explaining their meaning while illustrating how they can be used to address the stated problems. [ABSTRACT FROM AUTHOR]

This paper is a survey of several techniques that have proven useful in establishing compatibility among behaviorally similar programs (e.g., system upgrades, object sub- and supertypes, system components produced by different vendors, etc.). We give a comparative analysis of the techniques by evaluating their applicability to various aspects of the compatibility problemThe work described in section on substitutability check is based on a 2005 Formal Methods paper, Dynamic Component Substitutability, Lecture Notes in Computer Science 3582, 2005 by the same authors.. [ABSTRACT FROM AUTHOR]

XML transformations are most naturally defined as recursive functions on trees. A naive implementation, however, would load the entire input XML tree into memory before processing. In contrast, programs in stream processing style minimise memory usage since it may release the memory occupied by the processed prefix of the input, but they are harder to write because the programmer is left with the burden to maintain a state. In this paper, we propose a model for XML stream processing and show that all programs written in a particular style of recursive functions on XML trees, the macro forest transducer, can be automatically translated to our stream processors. The stream processor is declarative in style, but can be implemented efficiently by a pushdown machine. We thus get the best of both worlds — program clarity, and efficiency in execution. [ABSTRACT FROM AUTHOR]

Partial Redundancy Elimination (PRE) is a standard program optimization which removes redundant computations via Code Motion. It subsumes and generalizes the optimizations of Global Common Subexpression Elimination (GCSE) and Loop Invariant Code Motion (LICM). Recent work has generalized PRE to become Speculative PRE (SPRE), which uses estimates of execution frequencies to find the optimal places in a program to perform computations. However, the analysis performed by the compiler is computationally intensive and hence impractical for just-in-time (JIT) compilers. This paper introduces a novel approach which abandons a guarantee of optimality in favour of simplicity and speed of analysis. This new approach, called Isothermal SPRE, achieves results which are close to optimal in practice, yet its analysis time is at least as good as current compiler techniques for code motion. It is a technique suitable for use in JIT compilers. [ABSTRACT FROM AUTHOR]

For a long time, one of the major research goals in the computer science research community has been to raise the level of abstraction power of specification languages/programming languages. Many specification languages and formalisms have been invented, but unfortunately very few of those are practically useful, due to limited computer support of these languages and/or inefficient implementations. Thus, one important goal is executable specification languages of high abstraction power and with high performance, good enough for practical usage and comparable in execution speed to hand implementations of applications in low-level languages such as C or C++. In this paper we briefly describe our work in creating efficient executable specification languages for two application domains. The first area is formal specification of programming language semantics, whereas the second is formal specification of complex systems for which we have developed an object-oriented mathematical modeling language called Modelica, including architectural support for components and connectors. Based on these efforts, we are currently working on a unified equation-based mathematical modeling language that can handle modeling of items as diverse as programming languages, computer algebra, event-driven systems, and continuous-time physical systems. The key unifying feature is the notion of equation. In this paper we describe the design and implementation of the unified language. A compiler implementation is already up and running, and used for substantial applications. [ABSTRACT FROM AUTHOR]

Today's programming platforms do not provide sufficient constructs that allow a program's behavior to depend on the context in which it is executing. This paper presents the design and implementation of programming language extensions that explicitly support our vision of Context-oriented Programming. In this model, programs can be partitioned into layers that can be dynamically activated and deactivated depending on their execution context. Layers are sets of partial program definitions that can be composed in any order. Context-oriented Programming encourages rich, dynamic modifications of program behavior at runtime, requiring an efficient implementation. We present a dynamic representation of layers that yields competitive performance characteristics for both layer activation/deactivation and overall program execution. We illustrate the performance of our implementation by providing an alternative solution for one of the prominent examples of aspect-oriented programming. [ABSTRACT FROM AUTHOR]

Multimedia application development requires features and concepts currently not supported by common systems programming languages. This paper introduces two new minimal language extensions increasing expressive power, safety and optimization possibilities in multimedia programming. New loop statements are presented to shorten multidimensional array access and optimize its execution. Furthermore, a new data type concept is presented to allow quality of service (QoS) definition on data type declaration level. Both have been implemented in Modula-3 and C#. [ABSTRACT FROM AUTHOR]

Type abstraction in object-oriented languages mainly embodies two techniques with different strenghts and weaknesses. The first technique is extension, yielding abstraction mechanisms with good support for gradual specification; the prime example is inheritance. The second technique is functional abstraction, yielding more precise knowledge about the outcome; the prime example is type parameterized classes. This paper argues that they should be clearly separated to work optimally. We have applied this design philosophy to a language based on an extension mechanism, namely virtual classes. As a result, a kind of type parameters have been introduced, but they are simple and only used where they excel. Conversely, final definitions of virtual classes have been removed from the language, thus making virtual classes more flexible. The resulting language presents a clearer and more flexible trade-off between extensibility and predictability, empowering programmers to choose the right balance. [ABSTRACT FROM AUTHOR]

Exception handling is a well-established mechanism in sequential programming. Concurrency and asynchronous calls introduce a possibility for multiple simultaneous exceptions. This complicates exception handling, especially in languages whose support for exceptions has not originally been designed for concurrency. Futures are a mechanism for handling return values in asynchronous calls. They are affected by concurrent exception handling as well, since exceptions and return values are mutually exclusive in functions. This paper discusses these problems and presents a concurrent exception handling mechanism for future-based asynchronous C++ programs. [ABSTRACT FROM AUTHOR]

This paper shows that asynchronous fault detection is a practical way to reflect partial failure in a network-transparent distributed programming language. In the network-transparency approach, a program can be distributed over many sites without changing its source code. The semantics of the program's execution does not depend on how the program is distributed. We have experimented with various mechanisms for detecting and handling faults from within the language Oz. We present a new programming model that is based on asynchronous fault detection, is more consistent with the network-transparent nature of Oz, and improves the modularity of failure handling at the same time. [ABSTRACT FROM AUTHOR]

A remarkable result in [4] shows that in spite of its being less expressive than CCS w.r.t. weak bisimilarity, CCS! (a CCS variant where infinite behavior is specified by using replication rather than recursion) is Turing powerful. This is done by encoding Random Access Machines (RAM) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this paper we study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally show that the languages generated by termination-preserving CCS! processes are Type 1 . [ABSTRACT FROM AUTHOR]

Global value numbering (GVN) is an important static analysis technique both for optimizing compilers and program verification tools. Existing complete GVN algorithms discovering all Herbrand equivalences are all inefficient. One reason of this is the intrinsic exponential complexity of the problem, but in practice, since the exponential case is quite rare, the more important reason is the huge data structures annotated to every program point and slow abstract evaluations on them site by site. In this paper, we present an SSA-based algorithm for complete GVN, which uses just one global graph to represent all equivalences at different program points and performs fast abstract evaluations on it. This can be achieved because in SSA form, interferences among equivalence relations at different program points can be entirely resolved with dominance information. We implement the new algorithm in GCC. The average proportion of execution time of the new algorithm in the total compilation time is only 0.36%. To the best of our knowledge, this is the first practical complete GVN algorithm. [ABSTRACT FROM AUTHOR]

This paper shows the equivalence for provability between two infinitary systems with the ω-rule. One system is the positive one-sided fragment of Peano arithmetic without Exchange rules. The other system is two-sided Heyting Arithmetic plus the law of Excluded Middle for $\Sigma^0_1$-formulas, and it includes Exchange. Thus, the logic underlying positive Arithmetic without Exchange, a substructural logic, is shown to be a logic intermediate between Intuitionism and Classical Logic, hence a subclassical logic. As a corollary, the authors derive the equivalence for positive formulas among provability in those two systems and validity in two apparently unrelated semantics: Limit Computable Mathematics, and Game Semantics with 1-backtracking. [ABSTRACT FROM AUTHOR]

Gordon and Jeffrey developed a type system for checking correspondence assertions. The correspondence assertions, proposed by Woo and Lam, state that when a certain event (called an "end" event) happens, the corresponding "begin" event must have occurred before. They can be used for checking authenticity in communication protocols. In this paper, we refine Gordon and Jeffrey's type system and develop a polynomial-time type inference algorithm, so that correspondence assertions can be verified fully automatically, without any type annotations. The main key idea that enables polynomial-time type inference is to introduce fractional effects; Without the fractional effects, the type inference problem is NP-hard. [ABSTRACT FROM AUTHOR]

This paper studies types and probabilistic bisimulations for a timed π-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify the role of timers as interface between non-terminating and terminating communication for guaranteeing distributed liveness. We add message-loss probabilities to the calculus, and introduce a notion of approximate bisimulation that discards transitions below a certain specified probability threshold. We prove this bisimulation to be a congruence, and use it for deriving quantitative bounds for practical protocols in distributed systems, including timer-driven message-loss recovery and the Two-Phase Commit protocol. [ABSTRACT FROM AUTHOR]

Given the combinatorial nature of cellular signalling pathways, where biological agents can bind and modify each other in a large number of ways, concurrent or agent-based languages seem particularly suitable for their representation and simulation [1,2,3,4]. Graphical modelling languages such as κ [5, 6, 7, 8], or the closely related BNG language [9,10,11,12,13,14], seem to afford particular ease of expression. It is unclear however how such models can be implemented. Even a simple model of the EGF receptor signalling network can generate more than $\oldstylenums{10^{23}}$ non-isomorphic species [5], and therefore no approach to simulation based on enumerating species (beforehand, or even on-the-fly) can handle such models without sampling down the number of potential generated species. We present in this paper a radically different method which does not attempt to count species. The proposed algorothm uses a representation of the system together with a super-approximation of its ‘event horizon' (all events that may happen next), and a specific correction scheme to obtain exact timings. Being completely local and not based on any kind of enumeration, this algorithm has a per event time cost which is independent of (i) the size of the set of generable species (which can even be infinite), and (ii) independent of the size of the system (ie, the number of agent instances). We show how to refine this algorithm, using concepts derived from the classical notion of causality, so that in addition to the above one also has that the even cost is depending (iii) only logarithmically on the size of the model (ie, the number of rules). Such complexity properties reflect in our implementation which, on a current computer, generates about $\oldstylenums{10^6}$ events per minute in the case of the simple EGF receptor model mentioned above, using a system with $\oldstylenums{10^5}$ agents. [ABSTRACT FROM AUTHOR]

This paper presents the programming language Persistent Oberon, which offers persistence as a naturally inbuilt concept. Program data is automatically kept durable and stored in non-volatile memory, without the programmer having to write explicit code for the interactions with an external database system. In the case of a system interruption or failure, the program can directly continue from its latest consistent state. In contrast to other existent persistent programming languages, this language does not need any artificial programming interfaces or commands to use persistence. The programming language is completely implemented and offers a high scalability and performance. [ABSTRACT FROM AUTHOR]

Pattern matching makes ML programs more concise and readable, and these qualities are also sought in object-oriented settings. However, objects and classes come with open class hierarchies, extensibility requirements and the need for data abstraction, which all conflict with matching on concrete data types. Extractor-based pattern matching has been proposed to address this conflict. Extractors are user-defined methods that perform the task of value discrimination and deconstruction during pattern matching. In this paper, we give the first formalization of extractor-based matching, using a first-order object-oriented calculus. We give a direct operational semantics and prove it sound. We then present an optimizing translation to a target language without matching, and prove a correctness result stating that an expression is equivalent to its translation. [ABSTRACT FROM AUTHOR]

Metaprogramming and computational reflection are two related techniques that allow the programmer to change the semantics of a program in a modular fashion. Although the concepts have been explored by researchers for some time, a form of metaprogramming, namely aspect-oriented programming, is now being used by some practitioners. This paper is an attempt to understand the limitations of different forms of computational reflection in concurrent and distributed computing. It specifically studies the use of aspect-oriented programming and reflective actor libraries, and their relation to full reflection. We choose distributed monitoring as the primary example application because its requirements nicely fit the abilities of the two systems as well as illustrate their limitations. [ABSTRACT FROM AUTHOR]

In this paper we shall survey and discuss in detail the work on the relative expressiveness of recursion and replication in various process calculi. Namely, CCS, the π-calculus, the Ambient calculus, Concurrent Constraint Programming and calculi for Cryptographic Protocols. We shall give evidence that the ability of expressing recursive behaviour via replication often depends on the scoping mechanisms of the given calculus which compensate for the restriction of replication. [ABSTRACT FROM AUTHOR]

In this paper, we give an overview on some algorithms for learning automata. Starting with Biermann's and Angluin's algorithms, we describe some of the extensions catering for specialized or richer classes of automata. Furthermore, we survey their recent application to verification problems. [ABSTRACT FROM AUTHOR]

Rebeca is an actor-based language with a formal foundation for modeling concurrent and distributed systems which is designed in an effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported by a tool-set for model checking Rebeca models. Inherent characteristics of Rebeca are used to introduce compositional verification, abstraction, symmetry and partial order reduction techniques for reducing the state space. Simple message-driven object-based computational model, Java-like syntax, and set of verification tools make Rebeca an interesting and easy-to-learn model for practitioners. This paper is to present theories, applications, and supporting tools of Rebeca in a consistent and distilled form. [ABSTRACT FROM AUTHOR]

This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers. [ABSTRACT FROM AUTHOR]

Testing application behavior in the presence of I/O failures is extremely difficult. The resources used for testing usually work without failure. Failures typically cannot be initiated on the test suite level and are usually not tested sufficiently. Essentially, each interaction of the application with the environment can result in a failure. The Enforcer tool identifies such potential failures and automatically tests all relevant outcomes of such actions. It combines the structure of unit tests with coverage information and fault injection. By taking advantage of a unit test infrastructure, performance can be improved by orders of magnitude compared to previous approaches. This paper introduces the usage of the Enforcer tool. [ABSTRACT FROM AUTHOR]

In component-based development, the correctness of a system depends on the correctness of the individual components and on their interactions. Model-based testing is a way of checking the correctness of a component by means of executing test cases that are systematically generated from a model of the component. This model should include the behaviour of how the component can be invoked, as well as how the component itself invokes other components. In many situations, however, only a model that specifies how others can use the component, is available. In this paper we present an approach for model-based testing of components where only these available models are used. Test cases for testing whether a component correctly reacts to invocations are generated from this model, whereas the test cases for testing whether a component correctly invokes other components, are generated from the models of these other components. A formal elaboration is given in the realm of labelled transition systems. This includes an implementation relation, called eco, which formally defines when a component is correct with respect to the components it uses, and a sound and exhaustive test generation algorithm for eco. [ABSTRACT FROM AUTHOR]

Large-scale, value-added Internet services composed of independent cooperating or competing services will soon become common place. Several groups have addressed the performance, communication, discovery, and description aspects of these services. However, little work has been done on effectively composing paid services and the quality-of-service (QoS) guarantees that they provide. We address these issues in the context of distributed file storage in this paper. In particular, we propose, implement, and evaluate a cost-effective, QoS-aware distributed file service comprising a front-end file service and back-end (third-party) storage services. Our front-end service uses mathematical modeling and optimization to provide performance and availability guarantees at low cost by carefully orchestrating the accesses to the back-end services. Experimental results from our prototype implementation validate our modeling and optimization. We conclude that our approach for providing QoS at low cost should be useful to future composite Internet services. [ABSTRACT FROM AUTHOR]

Grids are becoming more and more dynamic, running parallel applications on large scale and heterogeneous resources. Explicitly stopping a whole distributed application is becoming increasingly difficult. In that context, there is a strong need to free resources a soon as they become useless, leading to automatic termination, using distributed garbage collecting techniques. We propose in this paper a new distributed garbage collector for active objects taking into account cycles but with a complexity similar to the distributed garbage collector of Java/RMI. The algorithm is based on a different approach to collect acyclic and cyclic garbage. On one hand, acyclic garbage is collected by knowing the immediate referencers of an active object and detecting the lack of these referencers. This behavior with respect to acyclic garbage is common to the distributed garbage collector of RMI. On the other hand, cyclic garbage is detected by considering the recursive closure of all the referencers of an active object and finding cycles of active objects waiting for requests. These cycles are found by letting idle active objects make a consensus on a common final activity. The algorithm is fully distributed and has been implemented with no modifications to the local garbage collector. Benchmarks have shown the scalability of the algorithm in a grid context. [ABSTRACT FROM AUTHOR]

Wireless sensor networks (WSNs) are evolving to support sense-and-react applications, where actuators are physically interspersed with the sensors that trigger them. This solution maximizes localized interactions, improving resource utilization and reducing latency w.r.t. solutions with a centralized sink. Nevertheless, application development becomes more complex: the control logic must be embedded in the network, and coordination among multiple tasks is needed to achieve the application goals. This paper presents TeenyLime, a WSN middleware designed to address the above challenges. TeenyLime provides programmers with the high-level abstraction of a tuple space, enabling data sharing among neighboring devices. These and other WSN-specific constructs simplify the development of a wide range of applications, including sense-and-react ones. TeenyLime yields simpler, cleaner, and more reusable implementations, at the cost of only a very limited decrease in performance. We support these claims through a source-level, quantitative comparison between implementations based on TeenyLime and on mainstream approaches, and by analyzing measures of processing overhead and power consumption obtained through cycle-accurate emulation. [ABSTRACT FROM AUTHOR]

Although unstructured Peer-to-Peer (P2P) networks provide economical platforms for supporting group communication applications, their ad-hoc nature poses significant challenges to the performance of the group communication services. This paper presents the design and implementation of GroupCast − a utility-aware middleware architecture for scalable and efficient P2P group communications. The GroupCast design is characterized by two unique features. First, we present a utility function for quantifying the role of unicast links in enhancing the scalability and efficiency of the group communication applications. Second, we develop a utility-aware distributed spanning tree construction algorithm for efficiently propagating group communication messages. It dynamically creates and maintains the group communication channels by optimizing the utility value of the group communication spanning trees. In addition, we also outline a utility-based overlay management protocol for constructing and maintaining low-diameter overlay networks. Our experiments show that the GroupCast system can improve the scalability of wide-area group communication services by one to two orders of magnitude. [ABSTRACT FROM AUTHOR]

Epidemic protocols have demonstrated remarkable scalability and robustness in disseminating information on internet-scale, dynamic P2P systems. However, popular instances of such protocols suffer from a number of significant drawbacks, such as increased message overhead in push-based systems, or low dissemination speed in pull-based ones. In this paper we study push-based epidemic dissemination algorithms, in terms of hit ratio, communication overhead, dissemination speed, and resilience to failures and node churn. We devise a hybrid push-based dissemination algorithm, combining probabilistic with deterministic properties, which limits message overhead to an order of magnitude lower than that of the purely probabilistic dissemination model, while retaining strong probabilistic guarantees for complete dissemination of messages. Our extensive experimentation shows that our proposed algorithm outperforms that model both in static and dynamic network scenarios, as well as in the face of large-scale catastrophic failures. Moreover, the proposed algorithm distributes the dissemination load uniformly on all participating nodes. [ABSTRACT FROM AUTHOR]

Content-based Publish/Subscribe (CPS) is a powerful paradigm providing loosely-coupled, event-driven messaging services. Although the general CPS model is well-known, many features remain implementation specific because of different application requirements. Many of these requirements can be captured in policies that separate service semantics from system mechanisms, but no such policy framework currently exists in the CPS context. In this paper, we propose a novel policy model and framework for CPS systems that benefits from the scalability and expressiveness of existing CPS matching algorithms. In particular, we provide a reference implementation and several evaluation scenarios that demonstrate how our approach easily and dynamically enables features such as notification semantics, meta-events, security zoning, and CPS firewalls. [ABSTRACT FROM AUTHOR]

Monitoring and management operations that query nodes based on their availability can be extremely useful in a variety of large-scale distributed systems containing hundreds to thousands of hosts, e.g., p2p systems, Grids, and PlanetLab. This paper presents decentralized and scalable solutions to a subset of such availability-based management tasks. Specifically, we propose AVMEM, which is the first availability-aware overlay to date. AVMEM is intended for generic non-cooperative scenarios where nodes may be selfish and may wish to route messages to a large set of other nodes, especially if the selfish node has low availability. Under this setting, our concrete contributions are the following: (1) AVMEM allows arbitrary classes of application-specified predicates to create the membership relationships in the overlay. In order to avoid selfish nodes from exploiting the system, we focus on predicates that are random and consistent. In other words, whether a given node y is a neighbor of a given node x is decided based on a consistent and probabilistic predicate, dependent solely on the identifiers and availabilities of these two nodes, but without using any external inputs. (2) AVMEM protocols discover and maintain the overlay spanned by the application-specified AVMEM predicate in a scalable and fast manner. (3) We use AVMEM to execute important availability-based management operations, focusing on range-anycast, range-multicast, threshold-anycast, and threshold-multicast. AVMEM works well in the presence of selfish nodes, scales to thousands of nodes, and executes each of the targeted operations quickly and reliably. Our evaluation is driven by real-life churn traces from the Overnet p2p system, and shows that AVMEM works well in practical settings. [ABSTRACT FROM AUTHOR]

Distributed computations, dealing with large amounts of data, are scheduled in Grid clusters today using either a task-centric mechanism, or a worker-centric mechanism. Because of the large data sets, the execution time is bounded by the cost of data transfer. In this paper, we introduce new worker-centric scheduling strategies that are novel in that they aim to implicitly exploit the locality of interest in order to reduce the cost of data transfer. Many Grid applications are characterized by such a locality of interest, i.e., a file is often accessed by multiple tasks and, more importantly, a set of files that are accessed by one task are also likely to be accessed together by other tasks. Our new deterministic, as well as probabilistic, scheduling algorithms implicitly exploit this feature to improve running time. Our experiments are done with traces of a real Grid application (Coadd), and show that our algorithms are able to achieve utilization of over 90%, while reducing makespan significantly compared to task-centric approaches. [ABSTRACT FROM AUTHOR]

The resource impoverished environment on mobile devices results in a poor experience for users browsing the World Wide Web. Proxy-based middleware that transform content on the fly to better suit the resource conditions on a user's device provide a promising solution to this problem. A key challenge in such systems is deciding how to adapt content, especially when the same content has multiple uses that have varying adaptation requirements. In this paper, we show that it is possible to provide fine grain adaptation of multi-purpose content by detecting correlations in the adaptation requirements of past users across multiple objects on a web site, and using this history to make adaptation predictions for users encountered subsequently. To evaluate our technique, we built prototype page layout and image fidelity adaptation systems, and used these to gather traces from users browsing multi-purpose web content in a laboratory setting. Our experimental results show that using correlations to make adaptation predictions can significantly reduce bandwidth consumption, browsing time, energy usage and user effort required to adapt content. [ABSTRACT FROM AUTHOR]

This paper describes the application of Real-Time Maude to the formal specification, simulation, and further formal analysis of the sophisticated state-of-the-art OGDC wireless sensor network algorithm. Wireless sensor networks in general, and the OGDC algorithm in particular, pose many challenges to their formal specification and analysis, including novel communication forms, treatment of geographic areas, time-dependent and probabilistic features, and the need to analyze both correctness and performance. Real-Time Maude extends the rewriting logic tool Maude to support formal specification and analysis of object-based real-time systems. This paper explains how we formally specified OGDC in Real-Time Maude, how we could simulate our specification to perform all the analyses done by the algorithm developers using the network simulation tool ns-2, and how we could perform further formal analyses which are beyond the capabilities of simulation tools. A remarkable result is that our Real-Time Maude simulations seem to provide a much more accurate estimate of the performance of OGDC than the ns-2 simulations. To the best of our knowledge, this is the first time a formal tool has been applied to an advanced wireless sensor network algorithm. [ABSTRACT FROM AUTHOR]

In this paper we propose a framework for modeling mobile information systems. Mobility introduces several challenges and issues that impact the development of mobile systems. As a result, we want applications running on mobile devices to exhibit certain traits; they should be aware of the mobility and be adaptive to the changes that occur due to it. Literature has identified several types of mobility - among them, physical and logical mobility. The former pertains to tangible mobile entities like cars, devices and people, while the latter encompasses mobile software entities. In addition to these, this paper includes the concept of vertical mobility - the movement of a network connection between overlapping networks - in a UML profile for modeling mobile information systems. We discuss our experiences from a case study described in [1] , where we modeled a simple mobile information system and transformed parts of the model into code. [ABSTRACT FROM AUTHOR]

Ubiquitous computing environments are characterised by a high number of heterogeneous devices that generate a huge amount of context data. These data are used to adapt applications to changing execution contexts. However, legacy frameworks fail to process context information in a scalable and efficient manner. In this paper, we propose to organise the classical functionalities of a context manager to introduce a 3-steps cycle of data collection, interpretation, and situation identification. We propose the COSMOS framework, which is based on the concepts of context node and context management policies translated into software components in software architecture. This paper presents COSMOS and evaluates its efficiency throughout the example of the composition of context information to implement a caching/off-loading adaptation situation. [ABSTRACT FROM AUTHOR]