Jul 152017

The paper entitled Interactive Runtime Verification has been accepted for publication in the proceedings of ISSRE 2017, the 28th International Symposium on Software Reliability Engineering (ISSRE) – IEEE. ISSRE will be held in Toulouse (France), October  23-26, 2017.

Below is an abstract of the paper:

Runtime Verification consists in studying a system at runtime, looking for input and output events to discover, check or enforce behavioral properties. Interactive debugging consists in studying a system at runtime in order to discover and understand its bugs and fix them, inspecting interactively its internal state.

Interactive Runtime Verification (i-RV) combines runtime verification and interactive debugging. We define an efficient and convenient way to check behavioral properties automatically on a program using a debugger. We aim at helping bug discovery and understanding by guiding classical interactive debugging techniques using runtime verification.

This is joint work with Raphaël Jakse, Jean-François Méhaut, and Kevin Pouget from Univ. Grenoble Alpes.

The preprint of the paper can be downloaded here.

Jul 012017

Our paper entitled Verifying Policy Enforcers has been accepted for publication in RV 2017, the 17th international conference on Runtime Verification.

Below is the abstract of the paper:

Policy enforcers are sophisticated runtime components that can prevent failures by enforcing the correct behavior of the software. While a single enforcer can be easily designed focusing only on the be- havior of the application that must be monitored, the effect of multiple enforcers that enforce different policies might be hard to predict. So far, mechanisms to resolve interferences between enforcers have been based on priority mechanisms and heuristics. Although these methods provide a mechanism to take decisions when multiple enforcers try to affect the execution at a same time, they do not guarantee the lack of interference on the global behavior of the system.
In this paper we present a verification strategy that can be exploited to discover interferences between sets of enforcers and thus safely identify a-priori the enforcers that can co-exist at run-time. In our evaluation, we experimented our verification method with several policy enforcers for Android and discovered some incompatibilities.

This is joint work with Oliviero Riganelli, Daniela Micucci, Leonardo Mariani from University of Milano Bicocca.

Jun 252017

The paper entitled “From high-level modeling toward efficient and trustworthy circuits” has been accepted for publication in Software Tools for Technology Transfer, a Springer journal.

Below is an abstract of the paper:

Behavior–interaction–priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. BIP framework comes with a runtime engine and a suite of verification tools that use D-Finder and NuSMV as model-checkers. In this paper, we provide a method and a supporting tool that take a BIP system and a set of invariants and compute a reduced sequential circuit with a system-specific scheduler and a designated output that is true when the invariants hold. Our method uses ABC, a sequential circuit synthesis and verification framework, to (1) generate an efficient circuit implementation of the system that can be readily translated into FPGA or ASIC implementations and to (2) verify the system and debug it in case a counterexample is found. Moreover, we generate a concurrent C implementation of the circuit that can be directly used for runtime verification. We evaluated our method with two benchmark systems, and our results show that, compared to existing techniques, our method is faster and scales to larger sizes.

The paper is now online on Springer Website.

One can also download the pre-print of the paper.

This is joint work with Fadi A. Zaraket, and Mohamad Jaber from American University of Beirut and Mohamad Noureddine from University of Illinois at Urbana Champaign.


May 302017

The paper entitled THEMIS: A Tool for Decentralized Monitoring Algorithms has been accepted as a tool-demonstration paper to ISSTA 2017, the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA 2017 will be held in Santa Barbara, California, USA, on July 10–14, 2017.

Below is an abstract of the paper:

THEMIS is a tool to facilitate the design, development, and analysis of decentralized monitoring algorithms; developed using Java and AspectJ. It consists of a library and command-line tools. THEMIS provides an API, data structures and measures for decentralized monitoring. These building blocks can be reused or extended to modify existing algorithms, design new more intricate algorithms, and elaborate new approaches to assess existing algorithms. We illustrate the usage of THEMIS by comparing two variants of a monitoring algorithm.

The pre-print of the paper can be downloaded on my publications Webpage.

THEMIS is open-source and available for download at https://gitlab.inria.fr/monitoring/themis.

This is joint work with A. El-Hokayem, Univ. Grenoble Alpes, Inria.

May 202017


 26th ACM SIGSOFT International Symposium on Software Testing and Analysis


 24th International SPIN Symposium on Model Checking of Software


 July 10-14, 2017, Santa Barbara, California, USA

ISSTA is the leading research symposium on software testing and analysis, bringing together academics, industrial researchers, and practitioners to exchange new ideas, problems, and experiences on how to analyze and test software systems.
The SPIN symposium brings together researchers and practitioners interested in automated, tool-based techniques to analyze software systems and models of software systems for verification and validation purposes.
  *** VENUE ***

University of California, Santa Barbara (www.ucsb.edu)


Registration is open! Early registration until June 9.



ISSTA list of accepted papers:

SPIN list of accepted papers:

    Christopher Kruegel, UCSB
    Armando Solar-Lezama, MIT
    Domagoj Babic, Google
    Byron Cook, Amazon Web Services
    Gerard Holzmann, Nimble Research

ISSTA Doctoral Symposium


ISSTA Demonstrations track


TECPS 2017: Workshop on Testing Embedded and Cyber-Physical Systems


RERS Challenge 2017: Rigorous Examination of Reactive Systems


Apr 292017

The paper entitled Monitoring Decentralized Specifications has been accepted for publication in the proceedings of ISSTA 2017, the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, which will be held in Santa Barbara, California, USA, on July 10–14, 2017.

The abstract of the paper is below:

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 the entire system. To do so, our approach introduces a data-structure that i) keeps track of the execution of an automaton, ii) has predictable parameters and size, and iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study decentralized monitorability, and present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Lastly, we introduce our tool, which is a framework for designing such decentralized algorithms, and simulating their behavior.

The pre-print of the paper can be downloaded on my publications Webpage.

This is joint work with Antoine El-Hokayem (Univ. Grenoble Alpes, Inria, Laboratoire d’Informatique de Grenoble).

Apr 172017

The paper entitled Formal analysis and offline monitoring of electronic exams has been accepted for publication in Formal Methods in System Design, a Springer journal.

The abstract of the paper is below:

More and more universities are moving toward electronic exams (in short e-exams). This migration exposes exams to additional threats, which may come from the use of the information and communication technology. In this paper, we identify and define several security properties for e-exam systems. Then, we show how to use these properties in two complementary approaches: model-checking and monitoring. We illustrate the validity of our definitions by analyzing a real e-exam used at the pharmacy faculty of University Grenoble Alpes (UGA ) to assess students. On the one hand, we instantiate our properties as queries for ProVerif, an automatic verifier of cryptographic protocols, and we use it to check our modeling of UGA exam specifications. ProVerif found some attacks. On the other hand, we express our properties as Quantified Event Automata (QEAs), and we synthesize them into monitors using MarQ, a Java tool designed to implement QEAs. Then, we use these monitors to verify real exam executions conducted by UGA. Our monitors found fraudulent students and discrepancies between the specifications of UGA exam and its implementation.

The preprint of the paper can be downloaded here.

This is joint work with Ali Kassem (Inria Grenoble) and Pascal Lafourcade (University of Clermont).

Apr 162017

The paper entitled Runtime Enforcement Using Büchi Games has been accepted for publication in SPIN 2017, the 24th International SPIN Symposium on Model Checking of Software.

Below is an abstract of the paper.

We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies. We present algorithms and a tool implementing enforcement mechanisms. We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing decisions of enforcement mechanisms ahead of time.

The preprint of the paper can be downloaded here.

This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux (France).

Apr 152017

The paper entitled Optimal Enforcement of (Timed) Properties with Uncontrollable Events has been accepted for publication in Mathematical Structures in Computer Science, a Cambridge University Press journal.

Below is the abstract of the paper:

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in defining and using mechanisms that modify the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property described by a deterministic automaton over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms should satisfy important properties, namely soundness, compliance, and optimality – meaning that enforcement mechanisms should output as soon as possible correct executions that are as close as possible to the input execution. We define the conditions for a property to be enforceable with uncontrollable events. Moreover, we synthesise sound, compliant, and optimal descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation.

This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux, Thierry Jéron and Hervé Marchand from Inria Rennes.