Ongoing research

Inspired by the $\pi$-calculus and by the coordination language Linda, the study of experimental languages for programming services over wide area network has been undertaken with the definition and implementation of the language KLAIM (in collaboration with the university of Florence). Special attention is given to types for access control. Models of computations for service-oriented computing have been also studied. A minimal set of primitives that allow capturing in an abstract way the ability to control and coordinate services in presence of QoS constraints have been identified. In particular, QoS requirements are expressed as distributed/concurrent constraints, which can be solved with efficient algorithms. The constraints are based on certain mathematical structures (c-semirings), where both classical and soft constraints can be expressed, thus representing features like costs, probabilities, preferences, and similar.

Also, the problem of negotiating and committing among multiple parties in a completely dynamic and open setting is studied, with particular focus on Long-Running Transactions (LRT), where transactional integrity is based on compensations. Key aspects of LRT are (forward and backward) workflow composition, fault handling mechanisms and commit protocols. It has been shown that commercial orchestration languages like BizTalk can be conveniently modeled with Zero-safe nets (ZSN) that were introduced in the past as a transactional extension of Petri nets. A novel, fully distributed commit protocol called D2PC has been invented and used to develop prototype implementations of ZSN in JOCAML and Polyphonic C#, that can also inter-operate across different platforms (Linux and .NET). The zero-safe approach has been exported to more expressive kinds of nets (contextual nets, colored nets, reconfigurable nets), to coordination languages (Linda) and to distributed mobile calculi (seen as a kind of higher-order, mobile version of nets). In particular, the latter research thread has led to the definition of committed Join (cJoin), an extension of Join calculus for which several type systems have been devised to guarantee serializability and fully distributed implementation. More recently, another research thread has started that focuses on the use of process algebras for modeling compensable flow composition and that has allowed to characterize in a formal way four different strategies for compensating parallel flows.

A general model of computation, called tile logic was introduced several years ago to provide a foundation for open, distributed and interactive systems. Tiles are rules defining the behavior of open configurations, i.e., system components, which may interact through their interfaces. Tiles can also be seen as double cells in double categories and research on tile logic includes work on algebraic and logical properties of monoidal, cartesian, cartesian closed double categories, which define different classes of tile models. In particular expressive tile models were found for non-interleaving process algebras (causal tree semantics) and logic programming. Also a coreflection has been observed between the categories of tiles and of rewriting systems. This universal construction allows us to see the same computation as a transaction (lower level) or as a transition (abstract level). Tile logic is executed by translating it into rewriting logic, which has quite efficient implementations. More recently, it has been shown that tile logic is a suitable framework for deriving congruence proofs of observational equivalences, thanks to the so-called tile decomposition property. In particular, it has been shown that double categories are the natural theoretical setting where to study the synthesis of bisimulation congruences from reactive systems (where only mute reductions are considered).

The approaches to compositionality typical of category theory (based on colimit constructions) and of process algebras (based on algebraic operations, on structured operational semantics and on structural axioms) have been compared employing the CommUnity connectors and the tile model. Suitable structural axioms have been derived which correspond to the colimit constructions.

We explore how coalgebraic techniques can be used for representing compositional, interactive systems. Ongoing studies show that coalgebras defined on a category of algebras are adequate for certain classes of specifications (which include and non-trivially generalize most formats used in process algebras by allowing structural axioms). This setting guarantees that bisimulation is a congruence with respect to the algebraic operators. In particular, sufficient conditions of wide applicability have been found which allow to lift a coalgebra from the category Set to the category of relevant algebras: essentially they require that structural axioms bisimulate. When name permutations are included in the algebraic operators, name handling (creation, passing, alpha conversion) becomes easier to represent. In particular bisimilarity for $\pi$-calculus and similar languages becomes expressible in purely coalgebraic ways, without crippling side conditions in its definition.

Certain classes of automata, called History Dependent (HD-) Automata have been introduced in the past, where both allocation and garbage collection of names are modeled. Process algebras with causality and locality information, Petri nets equipped with history preserving bisimulation, and synchronous and asynchronous $\pi$-calculus can be verified via HD-automata. Behavioral properties related to dynamic network connectivity, locality of resources and processes, and causality among events can be formally verified on finite HD-automata. Different versions of HD-automata have been defined to include name fusions and spatial operators. A further instance handling the symbolic semantics of nominal calculi has been recently introduced: this generalization of HD-automata can be conveniently applied to reason about web service discovery and binding. On the more foundational side, the relationships among several metamodels for calculi with name-passing have been investigated, including permutation algebras, named sets and sheaf categories, with the aim of establishing a bridge between such different approaches to the abstract specification of nominal calculi.

In the area of Petri nets, several variants of the basic models have been considered, including contextual nets (which can read tokens without consuming them), inhibitor nets (where the presence of a token on a place can inhibit the firing of a transition), and pre-nets, i.e., nets where a linear order is imposed on pre- and post-conditions of transitions. Several categorical constructions of ordinary nets have been generalized, to a certain extent, to such models, including adjunctions for the operational semantics and for the unfoldings in terms of event structures.

In the area of graph rewriting, the topics which are addressed range from the semantical foundations to their use for specifying and verifying concurrent and distributed systems. Concerning foundations, the emphasis is on generalizing analogous results for Petri nets. A concurrent semantics based on event structures, processes, and unfolding constructions has been developed. In particular, it has been shown that the construction of the associated event structure is a coreflection in the case of the single pushout approach, and only functorial in the double pushout approach. The generalization of these results to the abstract setting of rewriting systems based on Adhesive Categories is a topic of current research.

Concerning abstract semantics, history preserving bisimilarity, previously defined for contextual Petri nets, has been extended to graph transformations in the double pushout style. The construction often derives a finite HD-automaton, which can be minimized and model checked. A variant of the single pushout approach has been defined, called linear grammars for ordered graphs, which allows for a resource-conscious rewriting. For these grammars a tile-based semantics has been introduced, which allows for a universally defined operational semantics which guarantees compositionality via colimits.

Besides the single and double pushout approaches, also the Synchronized Hyperedge Replacement (SHR) approach is studied, and found particularly expressive for modeling software architectures and distributed, open and mobile systems. In particular it has been shown how it is strictly related to a particular interpretation of logic programming, which also allows for an efficient implementation. Synchronized hyperedge replacement has been used to provide an operational semantics to the architectural language Mobile CommUnity.

In order to generalise the synchronisation mechanism of SHR, the idea of synchronisation algebras has been extended to cope with mobility aspects introducing Synchronisation Algebras with Mobility (SAMs). This permits to use different SAMs inside the same graph so that heterogeneous systems can be modelled. Finally, QoS-based coordination of distributed activities has been achieved by using a specific class of SAMs corresponding to c-semiring

Several analysis and verification techniques have been studied, and also implemented in part, for both finite and infinite state systems.

HD-automata constitute the formal basis upon which several verification toolkits have been designed and implemented. The HAL toolkit supports verification by model checking of properties expressed as formulae of a suitable modal logic. HAL has been implemented in the past in collaboration with IEI-CNR (now ISTI-CNR). Within the European project PROFUNDIS, additional tools for automata minimization have been developed. Their design takes advantage of the foundational research about coalgebras. Also a general verification architecture is under experimentation. In this architecture the various verification tools are seen as web services available on the net and developed by geographically distributed sites. Verification applications are programmable via the coordination/orchestration languages previously mentioned, while distributed verification is clearly an interesting case study for coordination research.

For the verification of properties of distributed, mobile systems modeled with graph transformation, a methodology has been developed that can be applied to infinite state systems. Properties are expressed in a temporal logic which is a propositional $\mu$-calculus where the state predicates are formulae of a monadic second order logic, interpreted over graphs. The verification technique, applicable to a fragment of such logic, makes use of finite approximations of the unfolding of the graph transformation system. As a case study, the verification of the insertion operation into red-black trees as been addressed successfully.

An innovative notion of graph type has been introduced which adequately models software architectural styles. Software reconfigurations which preserve the style can be represented as typed graph transformations. Their correctness can be verified by proving a subject reduction properties on the transformation rules.

Symbolic verification techniques have been developed for the analysis of security protocols, that avoid the explicit construction of the whole, possibly infinite state-space of protocols. Based on these techniques verification toolkits have been implemented and successfully experimented on well-known protocols. A symbolic technique has been also studied to deal with the open-endness feature of distributed systems.

Also, static analysis techniques have been developed to check security properties. We studied access control, i.e., the problem of controlling the accesses to distributed resources. We considered mechanisms based on stack inspection, typical of programming languages like Java or C$_\char93$. We proposed a static analysis technique that approximates the sets of permissions that are enjoyed at certain program points, so improving the efficiency of stack inspection without compromising the secure access to resources. These optimizations include elimination of redundant checks or a different placing of them, dead code elimination, as well as more sophisticated optimizations like tail call elimination and method inlining. We also extended the $\lambda$-calculus with primitives for invoking services that respect given security requirements and we used type and effect systems to study secure composition of software.

Multi-algebras are also studied, which are an extension of standard algebras where operations return a set of results rather than a single result, and are useful for defining nondeterminism algebraically. For multi-algebras, Lawvere construction has been extended, by interpreting them as functors from certain categories weaker than cartesian. A simple inequational deduction system has also been derived for computing inclusions between relations computed by a multi-algebra, and it has been proved that term graphs provide a consistent and complete axiomatization.

We participate to the IST-FET-GC European project AGILE with research on graph rewriting, tiles, and their applications to software architectures of mobile and open systems based on wide area networks. In the area of graph rewriting and visual systems we are also partners of the European RTN network SEGRAVIS. We contributed with a total of three chapters to the Handbooks on graph rewriting, edited by Grzegorz Rozenberg and others.

We partecipate to the Italian Ministry for the University PRIN ART. The goal of the project is to analyse the foundational issues concerning the use of reduction systems (RS) and labeled transition systems (LTS) for the modeling of computational devices. More specifically, the research landscape is represented by the widespread diffusion of RSs as a tool for describing the operational semantics of a system, and the reckoning of their lack of suitable abstract semantics. The starting point is represented by the recent advances on the synthesis of an LTS from an RS, and the theoretical work that has been pursued in the analysis of the resulting observational semantics.

We participate to the FET-GC2 Integrated Project SENSORIA whose overall aim is to develop a novel comprehensive approach to the engineering of software systems for service-oriented overlay computers where foundational theories, techniques and methods are fully integrated in a pragmatic software engineering approach. It focuses on global services that are context-adaptive, personalisable, and may require hard and soft constraints on resources and performance, and it takes into account the fact that services have to be deployed on different, possibly interoperating, global computers, to provide novel and reusable service-oriented overlay computers.

Within SENSORIA our main contribution addresses the development of a foundational methodology for describing service specifications, for developing their disciplined composition and for the quantitative and qualitative analysis of combined services.