As the concept of Service Oriented Computing matures the need for well defined architectures and protocols to address this trend is essential if IT is going to properly embrace SOC. The SOC paradigm has several requirements to work properly such as service composition and cooperation in a loosely coupled fashion, ability to adapt autonomously to environmental and business changes and address concerns such as modularity, dynamicity and proper integration between services. The popularization of the OSGi platform its another effort towards the SOC paradigm by issuing key aspects such as modularity and dynamicity in its service oriented design. However there is much room for improvement namely on the creation of architectures and mechanisms to improve the dependability of the overall solution by strengthening key properties such as the availability, reliability, integrity, safety and maintainability of the platform. In this work we propose a middleware layer that offers the strong modular and dynamic properties required in an SOC environment by relying on OSGi while addressing dependability concerns. The starting point to achieve this is by instrumenting an OSGi implementation and providing means to monitor and manage it accordingly to business and environmental requirements. By relying on group communication facilities and some properties from the OSGi specification we are able to migrate OSGi environments between nodes thus minimizing service delivery disruption in the presence of faults and addressing, at the same time SLA properties by migrating (or shutting down) services that are consuming more resources than agreed/expected.
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.
Invariants, bisimulations and assertions are the main ingredients of coalgebra theory applied to software systems. In this paper we reduce the first to a particular case of the second and show how both together pave the way to a theory of coalgebras which regards invariant predicates as types. An outcome of such a theory is a calculus of invariants’ proof obligation discharge, a fragment of which is presented in the paper.The approach has two main ingredients: one is that of adopting relations as “first class citizens” in a pointfree reasoning style; the other lies on a synergy found between a relational construct, Reynolds’ relation on functions involved in the abstraction theorem on parametric polymorphism and the coalgebraic account of bisimulations and invariants. This leads to an elegant proof of the equivalence between two different definitions of bisimulation found in coalgebra literature (due to B. Jacobs and Aczel & Mendler, respectively) and to their instantiation to the classical Park-Milner definition popular in process algebra.
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.
COORDINSPECTOR is a Software Tool aiming at extracting the coordination layer of a software system. Such a reverse engineering process provides a clear view of the actually invoked services as well as the logic behind such invocations. The analysis process is based on program slicing techniques and the generation of, system dependence graphs and coordination dependence graphs. The tool analyzes common intermediate language (CIL), the native language of the Microsoft .Net Framework, thus making suitable for processing systems developed in any .Net Framework compilable language. COORDINSPECTOR generates graphical representations of the coordination layer together with business process orchestrations specified in WSBPEL 2.0.
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.
Although increasingly popular, Model Driven Architecture (MDA) still lacks suitable formal foundations on top of which rigorous methodologies for the description, analysis and transformation of models could be built. This paper aims to contribute in this direction: building on previous work by the authors on coalgebraic refinement for software components and architectures, it discusses refactoring of models within a coalgebraic semantic framework. Architectures are defined through aggregation based on a coalgebraic semantics for (subsets of) UML. On the other hand, such aggregations, no matter how large and complex they are, can always be dealt with as coalgebras themselves. This paves the way to a discipline of models’ transformations which, being invariant under either behavioural equivalence or refinement, are able to formally capture a large number of refactoring patterns. The main ideas underlying this research are presented through a detailed example in the context of refactoring of UML class 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.
Current software development relies increasingly on non-trivial coordination logic for combining autonomous services often running on different platforms. As a rule, however, intypical non-trivial software systems, such a coordination layer is strongly weaved within the application at source code level. Therefore, its precise identification becomes a major methodological (and technical) problem which cannot be overestimated along any program understanding or refactoring process. Open access to source code, as granted in OSS certification, provides an opportunity for the development of methods and technologies to extract, from source code, the relevant coordination information. This paper is a step in this direction, combining a number of program analysis techniques to automatically recover coordination information from legacy code. Such information is then expressed as a model in Orc, a general purpose orc hestration language.
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.
Causality tracking mechanisms, such as vector clocks and version vectors, rely on mappings from globally unique identifiers to integer counters. In a system with a well known set of entities these ids can be preconfigured and given distinct positions in a vector or distinct names in a mapping. Id management is more problematic in dynamic systems, with large and highly variable number of entities, being worsened when network partitions occur. Present solutions for causality tracking are not appropriate to these increasingly common scenarios. In this paper we introduce Interval Tree Clocks, a novel causality tracking mechanism that can be used in scenarios with a dynamic number of entities, allowing a completely decentralized creation of processes/replicas without need for global identifiers or global coordination. The mechanism has a variable size representation that adapts automatically to the number of existing entities, growing or shrinking appropriately. The representation is so compact that the mechanism can even be considered for scenarios with a fixed number of entities, which makes it a general substitute for vector clocks and version vectors.
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.
Computational Design (CD) is a paradigm where both program design and program synthesis are computations. CD merges Model Driven Engineering (MDE) which synthesizes programs by transforming models, with Software Product Lines (SPL) where programs are synthesized by composing transforma tions called features. In this paper, basic relationships between MDE and SPL are explored using the language of modern mathematics.
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.
We present a novel coalgebraic logic for deterministic Mealy machines that is sound, complete and expressive w.r.t. bisimulation. Every finite Mealy machine corresponds to a finite formula in the language. For the converse, we give a compositional synthesis algorithm which transforms every formula into a finite Mealy machine whose behaviour is exactly the set of causal functions satisfying the formula.