From Global Choreographies to Verifiable Efficient Distributed Implementations

Paper From Global Choreographies to Veri able Efficient Distributed Implementations has been accepted for publication in the Journal of Logical and Algebraic Methods in Programming. The abstract of the paper is below. We define a method to automatically synthesize efficient distributed implementations from high-level global choreographies. A global choreography describes the execution and communication logic between a set […]

Read More

A survey of challenges for runtime verification from advanced application domains (beyond software)

The paper A survey of challenges for runtime verification from advanced application domains (beyond software) has been published in Formal Methods in System Design, a Springer journal. The paper can be downloaded by following this link. This is joint work with César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, Ezio Bartocci, Domenico Bianculli, Christian Colombo, Adrian Francalanza, […]

Read More

On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation

The paper On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation has been accepted for publication in TOSEM, the ACM Transactions on Software Engineering and Methodology. We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of […]

Read More

On the Runtime Enforcement of Timed Properties

The tutorial paper On the Runtime Enforcement of Timed Properties has been accepted for publication in Runtime Verification 2019. Runtime enforcement refers to the theories, techniques, and tools for enforcing correct behavior of systems at runtime. We are interested in such behaviors described by specifications that feature timing constraints formalized in what is generally referred […]

Read More

Tracing Distributed Component-Based Systems, a Brief Overview

The paper Tracing Distributed Component-Based Systems, a Brief Overview has been accepted for publication in the Proceedings of the 18th International Conference on Runtime Verification. The abstract of the paper is below: We overview a framework for tracing asynchronous distributed component-based systems with multiparty interactions managed by distributed schedulers. Neither the global state nor the total ordering […]

Read More

Bringing Runtime Verification Home

The paper Bringing Runtime Verification Home has been accepted for publication in the Proceedings of the 18th International Conference on Runtime Verification. Below is the abstract of the paper: We use runtime verification (RV) to check various specifications in a smart apartment. The specifications can be broken down into three types: behavioral correctness of the apartment sensors, […]

Read More

Facilitating the implementation of distributed systems with heterogeneous interactions

The paper Facilitating the implementation of distributed systems with heterogeneous interactions has been accepted for publications in the proceedings of iFM 2018, the 14th International Conference on integrated Formal Methods. iFM 2018 will be held on 5th -7th September 2018, in Maynooth University, Ireland. Below is the abstract of the paper: We introduce HDBIP an extension of the Behavior Interaction […]

Read More

Modularizing Behavioral and Architectural Crosscutting Concerns in Formal Component-Based Systems

The paper entitled Modularizing Behavioral and Architectural Crosscutting Concerns in Formal Component-Based Systems – Application to the Behavior Interaction Priority Framework has been accepted for publication in Journal of Logical and Algebraic Methods in Programming (Elsevier) The abstract of the paper is below: We define a method to modularize crosscutting concerns in Component-Based Systems (CBSs) expressed using the […]

Read More