Pedro Martins

Adaptation of system parameters is acknowledged as a requirement to scalable and dependable distributed systems. Unfortunately, adaptation cannot be effective when provided solely by individual system components as the correct decision is often tied to the composition itself and the system as a whole. In fact, proper adaption is a cross-cutting issue: Diagnostic and feedback operations must target multiple components and do it at different abstraction levels. We address this problem with the Serpentine middleware platform. By relying on the industry standard JMX as a service interface, it can monitor and operate on a wide range of distributed middleware and application components. By building on a JMX-enabled OSGi runtime, Serpentine is able to control the life-cycle of components themselves. The scriptable stateless server and cascading architecture allow for increased dependability and flexibility.

More and more current software systems rely on non trivial coordination logic for combining autonomous services typically running on different platforms and often owned by different organizations. Often, however, coordination data is deeply entangled in the code and, therefore, difficult to isolate and analyse separately.
COORDINSPECTOR is a software tool which combines slicing and program analysis techniques to isolate all coordination elements from the source code of an existing application. Such a reverse engineering process provides a clear view of the actually invoked services as well as of the orchestration patterns which bind them together.
The tool analyses Common Intermediate Language (CIL) code, the native language of Microsoft .Net Framework. Therefore, the scope of application of COORDINSPECTOR is quite large: potentially any piece of code developed in any of the pro- gramming languages which compiles to the .Net Framework. The tool generates graphical representations of the coordination layer together and identifies the underlying business process orchestrations, rendering them as Orc specifications.

If, as a well-known aphorism states, modelling is for reasoning , this paper is an attempt to define and apply a formal semantics to UML sequence diagrams in order to enable rigourous reasoning about them. Actually, model transfor- mation plays a fundamental role in the process of software development, in general, and in model driven engineering in particular. Being a de facto standard in this area, UML is no exception, even if the number and diversity of diagrams expressing UML models makes it difficult to base its semantics on a single framework. This paper builds on previous attempts to base UML semantics in a coalgebraic setting and illustrates the application of the proposed framework to reason about composition and refactoring of sequence diagrams.

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In par- ticular, it allows for reasoning about confinement in object- oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

In the algebraic specification of software systems, it is desirable to have freedom in the implementation process, namely for the software reuse. In this paper we will discuss two issues in order to achieve this freedom: we study the observational stepwise refinement process and we propose an alternative formalization of the refinement concept based on the logical translation from the abstract algebraic logic. In the first topic, we go beyond the traditional assumption of maintaining the set of observable sorts during the refinement process by the possibility of changing it between the process steps, i.e., we analise the stepwise refinement with encapsulation and desencapsulation of sorts during the process. In the second topic, we suggest a formalization of the refinement con- cept where an equation may be mapped into a set of equations, against the refinements based on signature morphisms, where an equation is mapped into another one.

Programming directly with diagrams offers potential advantages such as visual intuitions, identification of errors (debugging), and insight into the dynamics of the algorithm. The purpose of this paper is to put forward one particular graphical formalism, interaction nets, as a candidate for visual programming which has not only all the desired properties that one would expect, but also has other benefits as a language, for instance sharing computation.

Molecular dynamics simulations is a valuable tool to study protein unfolding in silico. Analyzing the relative spatial position of the residues during the simulation may indicate which residues are essential in determining the protein structure. We present a method, inspired by a popular data mining technique called Frequent Itemset Mining, that clusters sets of amino acid residues with a synchronized trajectory during the unfolding process. The proposed approach has several advantages over traditional hierarchical clustering.