Runtime Enforcement with Reordering, Healing, and Suppression

The paper entitle “Runtime Enforcement with Reordering, Healing, and Suppression” has been accepted for publication in the proceedings of the 19th International Conference on Software Engineering and Formal Methods. The paper abstract is below: Runtime enforcement analyses an execution trace, detects when this execution deviates from its expected behaviour with respect to a given property, […]

Read More

Monitoring Distributed Component-Based Systems

The paper entitled Monitoring Distributed Component-Based Systems has been accepted for publication in the proceedings of the 17th edition of the International Conference on Formal Aspects of Component Software (FACS). Abstract of the paper is below We monitor asynchronous distributed component-based systems with multi-party interactions. We consider independent components whose interactions are managed by several […]

Read More

Decentralized LTL Enforcement

Paper Decentralized LTL Enforcement has been accepted for publication in the proceedings of GandALF’21, the 12th International Symposium on Games, Automata, Logics, and Formal Verification. The abstract is below: We consider the runtime enforcement of Linear-time Temporal Logic formulas on decentralized systems with no central observation point nor authority. A so-called enforcer is attached to each […]

Read More

BISM: Bytecode-Level Instrumentation for Software Monitoring

The paper entitled “BISM: Bytecode-Level Instrumentation for Software Monitoring” has been accepted for publication in the proceedings of RV’20, the 20TH international conference on Runtime Verification. The abstract of the paper is below: BISM (Bytecode-Level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool which features an expressive high-level control-flow-aware instrumentation language. The language […]

Read More

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

Runtime enforcement of timed properties using games

The paper Runtime enforcement of timed properties using games has been accepted for publication in Format Aspect of Computing. The abstract of the paper is below. This paper deals with runtime enforcement of timed properties with uncontrollable events. Runtime enforcement consists in defining and using an enforcement mechanism that modifies the executions of a running system […]

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