Recent Publications

Matos M, Sousa AL.  2008.  Dependable distributed OSGi environment. Proceedings of the 3rd workshop on Middleware for service oriented computing - MW4SOC. :1–6. Abstractmw4soc-ddosgi.pdf

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.

Matos M, Correia A, Pereira JO, Oliveira R.  2008.  Serpentine: adaptive middleware for complex heterogeneous distributed systems. SAC '08: Proceedings of the 2008 ACM symposium on Applied computing. :2219–2223. Abstractsac-serpentine.pdf

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.

Barbosa LS, Oliveira JN, Silva A.  2008.  Calculating invariants as coreflexive bisimulations. Proceedings of 12th International Conference on Algebraic Methodology and Software Technology - AMAST . 5140:83–99. Abstractamast08-bos.pdf

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.

Rodrigues N, Barbosa LS.  2008.  CoordInspector: a tool for extracting coordination data from legacy code. 8th IEEE International Working Conference on Source Code Analysis and Manipulation - SCAM . :265-266. Abstractscam08-rb.pdf

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.

Rodrigues N, Barbosa LS.  2008.  On the Discovery of Business Processes Orchestration Patterns. IEEE Congress on Services - SERVICES . :391-398. Abstractrb08a.pdf

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.

Meng S, Barbosa LS.  2008.  A Coalgebraic Semantic Framework for Reasoning about {UML} Sequence Diagrams. Proceedings of the 8th International Conference on Quality Software - QSIC. :17-26. Abstractqsic08-mb.pdf

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.

Barbosa LS, Meng S.  2008.  UML Model Refactoring as Refinement: A Coalgebraic Perspective. 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - SYNASC . :340-347. Abstract10.1.1.205.5454.pdf

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.

Wang S, Barbosa LS, Oliveira JN.  2008.  A relational model for confined separation logic. 2nd IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering - TASE. :263-270. Abstracttase08-wbo.pdf

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.

Rodrigues N, Barbosa LS.  2008.  Extracting and verifying coordination models from source code. Proceedings of FLOSS-FM/OpenCert Joint International Workshop at OOS'08. :64-78. Abstractrb08b.pdf

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.

Madeira A.  2008.  Observational Refinement Process. International Workshop in Refinements. 214:103-129. Abstractobservational_refinement_process.pdf

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.

Almeida PS, Moreno CB, Fonte V.  2008.  Interval tree clocks. 12th International Conference on Principles of Distributed Systems - OPODIS. 5401 Abstractitc.pdf

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.

Pinto JS, Mackie I, Hassan A.  2008.  Visual programming with interaction nets. 5th International Conference on the Theory and Application of Diagrams. Abstractvispin-diagrams08.pdf

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.

Saraiva JA, Azanza M, Batory DS.  2008.  The objects and arrows of computacional design. Proceedings of 11th International Conference, MoDELS 2008. Abstractfulltext.pdf

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.

Ferreira P, Silva C, Azevedo PJ, Brito R.  2008.  Spatial Clustering of Molecular Dynamics Trajectories in Protein Unfolding Simulations. 5th International Meeting on Computacional Intelligence Methods for Bioinformatics and Biostatistics - CIBB. Abstractspatialclustering.pdf

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.

Bonsangue M, Rutten J, Silva A.  2008.  Coalgebraic logic and synthesis of mealy machines. Proceedings of the Eleventh International Conference on Foundations of Software Science and Computation structures (FoSSaCS 2008). 4962:231–245. Abstractmealy.pdf

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.