Catálogo de publicaciones - libros

We statically check whether each component in a component-based system is used according to its protocol and provide counterexamples if such a check fails. The protocol is given by a finite state machine specifying legal sequences of procedure calls of the interface of a component. The main contribution is that we can deal with call-backs without any restrictions. We achieved this by using context-free grammars instead of finite state machines to describe the use of components.

Component-Based Software Engineering (CBSE) is one of the approaches to master the development of large scale software. In this setting, the verification concern is still a challenge. The current work addresses the composability of components and their services. A component model (Kmelia) is introduced; an associated formalism, simple but expressive is introduced; it describes the services as extended LTSs and their structuring as components. The composability of components is defined on the basis of the composability of services. To ensure the correctness of component composition, we check that an assembly is possible via the checking of the composability of the linked services, and their behavioural compatibility. In order to mechanize our approach, the services and the components are translated into the formalism. Finally the CADP toolbox is used to perform experiments.

To maintain loose coupling and facilitate dynamic composition, components in a pipe-and-filter architecture have a very limited syntactic interface and often communicate indirectly by means of a shared data repository. This severely limits the possibilities for compile time compatibility checking. Even static type checking is made largely irrelevant due to the very general types given in the interfaces. The combination of pipe-and-filter and a shared data repository is widely used, and in this paper we study this problem in the context of the Struts framework. We propose simple, but formally specified, behavioural contracts for components in such frameworks and show that automated formal verification of certain semantical compatibility properties is feasible. In particular, our verification guarantees that indirect data sharing through the shared data repository is performed consistently.

Using different specification formalisms together is necessary to leverage better reliability on component-based systems. The system provides a contracting system for hierarchical software components, but currently, only executable assertions are supported.

In this paper, we describe how TLA, taken as an instance of behavioral sequence-based formalism, was integrated in . A domain specific language is proposed in order to enable designers to describe the observations needed to appropriately verify their specifications. These observations are automatically generated for assertions and in the case of TLA, we show what kind of observations must be provided to link the specifications to the concrete application.

One of the main problems in Aspect-Oriented Software Development is the so-called fragile pointcut problem. Uncovering and specifying a good robust pointcut is not an easy task. In this paper we propose to use Inductive Logic Programming, and more specifically the FOIL algorithm, to automatically identify intensional (or “pattern-based”) pointcuts. We present the tool chain we implemented to induce a pointcut given a set of identified joinpoints. Using several realistic medium-scale experiments, we show that our approach is able to automatically induce robust pointcuts for a set of joinpoints.

Nowadays, application developers have to deal with increasingly variable execution contexts, requiring the creation of applications able to adapt themselves autonomously to the evolutions of this context. In this paper, we show how an aspect-oriented approach enables the development of self-adaptive applications where the adaptation code is well modularized, both spatially and temporally. Concretely, we propose SAFRAN, an extension of the Fractal component model for the development of the adaptation aspect as reactive adaptation policies. These policies detect the evolutions of the execution context and adapt the base program by reconfiguring it. This way, SAFRAN allows the modular development of adaptation policies and their dynamic weaving into running applications.

Aspect composition is a challenging and multi-faceted issue, generally under-supported by current AOP languages and frameworks. This paper presents the composition support provided in Reflex, a versatile kernel for multi-language AOP in Java. The core of Reflex is based on a model of partial reflection whose central abstractions are links: bindings between a (point)cut and an action. Reflex supports the definition of aspect languages through the mapping of aspects to links. We overview the wide range of features for link composition in Reflex—which includes extensible operators for ordering and nesting of links, and control over the visibility of changes made by structural aspects—, illustrating how they can be used to implement various scenarios of aspect composition.

This paper tackles the problem of composition of transaction services, which are governed by various transaction standards. Among others, we can cite the , , or . However, the Web Services Atomic Transaction standard encloses legacy transaction standards to support the Web Services application platform. This encapsulation introduces an additional complexity to the system and hides the specificities of legacy transaction standards. When composing heterogeneous legacy applications, the underlying transaction services are basically not composed transparently. This paper presents an approach to build an , named ATS, which supports several transaction standards concurrently. The objective of ATS is to facilitate the transaction standards composition. To introduce ATS we detail how the Object Transaction Service, Web Services Atomic Transaction, and Java Transaction Service standards can be composed. Besides, an ATS implementation is introduced using the GoTM framework. We show that this fine-grained component-based approach does not introduce an additional overhead to legacy applications and supports well scalability. Moreover, this approach can be extended to other standards.

To be able to compose and decompose software components at run time, some form of between components (or objects) is needed. In this paper, we identify basic properties of dynamic object (re)binding, and propose a class-based object calculus that gives precise meaning to these properties. We also define two example semantic properties that are characteristic for many concurrent programs with low-level bind/unbind operations. Our calculus has a built-in construct that can be used to implement one of the semantic properties.

are a formalism based on linear temporal logic (LTL) with variable bindings and pointcuts of the aspect-oriented language AspectJ for the purpose of verification. We demonstrate how tracechecks can be used to model . These assertions reason about the dynamic control flow of an application. They can be used to formally define the semantic interface of classes. We explain in detail how we make use of AspectJ pointcuts to derive a formal model of an existing application and use LTL to express temporal assertions over this model.

We developed a reference implementation with the compiler showing that the tool can be applied in practice and is memory-efficient.

In addition we show how tracechecks can be deployed as Java5 annotations, yielding a system which is fully compliant with any Java compiler and hiding any peculiarities of aspect-oriented programming from the user. Through annotations, the tracecheck specifications become a semantic part of an interface. Consumers of such a component can then take advantage of the contained annotations by applying our tool and have their use of this component automatically checked at runtime for compliance with the intent of the component provider.