My talk on “State Space C-Reductions for Concurrent Systems in Rewriting Logic” held at the International ETAPS Workshop on Graph Inspection and Traversal Engineering (GRAPHITE 2013).
Full manuscript available here: http://eprints.imtlucca.it/1350/
Assistant Professor @ IMT Lucca
The slides of my talk on Adaptable Transition Systems at the ASCENS General and Working Meeting.
The slides of my talk on white-box adaptation at the kick-off meeting of the Italian PRIN project CINA.
I am happy to be involved in the 4th International Workshop on Modeling and Simulation of Peer-to-Peer and Autonomic Systems (MOSPAS 2013) to be held on July 1 – 5, 2013 in Helsinki, Finland (colocated with HPCS 2013).
Submission deadline is March 01, 2013.
Our work on Adaptable Transition Systems has been accepted for the WADT 2012 proceedings. Here’s the abstract
We present adaptable transition systems (ATSs), an essential model of adaptive systems inspired by white-box approaches to adaptation (like control data) and based on foundational models of component based systems (like I/O automata and interface automata). The key feature of atss are control propositions, the formal counterpart of control data. The choice of control propositions is arbitrary, but it imposes a clear separation between ordinary, functional behaviors and adaptive ones. We discuss how atss can be exploited in the specification and analysis of adaptive systems, focusing on various notions proposed in the literature, like adaptability, feedback loops, and control synthesis.
Our work on A cooperative approach for distributed task execution in autonomic clouds has been accepted for presentation at the 21st Euromicro International Conference on Parallel, Distributed, and Network-Based Processing PDP 2013 (PDP 2013). Here’s the abstract
Virtualization and distributed computing are two key pillars that guarantee scalability of applications deployed in the Cloud. In Autonomous Cooperative Cloud-based Platforms, autonomous computing nodes cooperate to offer a PaaS Cloud for the deployment of user applications. Each node must allocate the necessary resources for customer applications to be executed with certain QoS guarantees. If the QoS of an application can not be guaranteed a node has mainly two options: to ask for more resources (if it is possible) or to rely on the collaboration of other nodes. This decision is not trivial since it involves many factors (e.g. the cost of setting up virtual machines, migrating applications, discovering collaborators, etc.). In this paper we present a model of such scenarios and experimental results validating the convenience of cooperative strategies over selfish ones. We describe the architecture of the platform of autonomous clouds and the main features of the model, which has been implemented in the DEUS discrete-event simulator, for being evaluated.
Our work on Exploiting over- and under-approximations for infinite-state counterpart models has been accepted for presentation at the 6th International Conference on Graph Transformations (ICGT 2012). Here’s the abstract
Software systems with dynamic topology are often infinite-state. Paradigmatic examples are those modeled as graph transformation systems (GTSs) with rewrite rules that allow an unbounded creation of items. For such systems, verification can become intractable, thus calling for the development of approximation techniques that may ease the verification at the cost of losing in preciseness and completeness. Both over- and under-approximations have been considered in the literature, respectively offering more and less behaviors than the original system. At the same time, properties of the system may be either preserved or reflected by a given approximation. In this paper we propose a general notion of approximation that captures some of the existing approaches for GTSs. Formulae are specified by a generic quantified modal logic that generalizes many specification logics adopted in the literature for GTSs. We also propose a type system to denote part of the formulae as either reflected or preserved, together with a technique that exploits under- and over-approximations to reason about typed as well as untyped formulae.
Our work on State Space c-Reductions of Concurrent Systems in Rewriting Logic has been accepted for presentation at the 14th International Conference on Formal Engineering Methods (FASE 2012). Here’s the abstract
We present c-reductions, a simple, flexible and very general state space reduction technique that exploits an equivalence relation on states that is a bisimulation. Reduction is achieved by a canonizer function, which maps each state into a not necessarily unique canonical representative of its equivalence class. The approach contains symmetry reduction and name reuse and name abstraction as special cases, and exploits the expressiveness of rewriting logic and its realization in Maude to automate c-reductions and to seamlessly integrate model checking and the discharging of correctness proof obligations. The performance of the approach has been validated over a set of representative case studies.
The slides of my lecture at the AWASS 2012 Summer School on Self-Awareness in Autonomic Computing.