Aug 282017

ETR is a well-known Frenh summer school on real-time systems and formal methods. I am giving a tutorial talk in the formal methods track about Runtime Enforcement of Timed Properties.

The companion tutorial can be found in the proceedings and the electronic version can be downloaded here.

Aug 102017

Our journal paper entitled Decentralized Enforcement of Document Lifecycle Constraints has been accepted for publication in Information Systems, an Elsevier journal.

Below is an abstract of the paper:

Artifact-centric workflows describe possible executions of a business process through constraints expressed from the point of view of the documents exchanged between principals. A sequence of manipulations is deemed valid as long as every document in the workflow follows its prescribed lifecycle at all steps of the process. So far, establishing that a given workflow complies with artifact lifecycles has mostly been done through static verification, or by assuming a centralized access to all artifacts where these constraints can be monitored and enforced. We present in this paper an alternate method of enforcing document lifecycles that requires neither static verification nor single-point access. Rather, the document itself is designed to carry fragments of its history, protected from tampering using hashing and public-key encryption. Any principal involved in the process can verify at any time that the history of a document complies with a given lifecycle. Moreover, the proposed system also enforces access permissions: not all actions are visible to all principals, and one can only modify and verify what one is allowed to observe. These concepts have been implemented in a software library called Artichoke, and empirically tested for performance and scalability.

This is joint work with Sylvain Hallé, Raphaël Khoury, Quentin Betty from Université du Quebec at Chicoutimi, and Antoine El-Hokayem from Univ. Grenoble Alpes.

Jul 232017


Topic E3: Model-based Design and Verification for Embedded Systems

at DATE 2018,
Dresden, GE
March 19 – 23, 2018

DATE 2018, will take place from 19 to 23 March, 2018, at the International Congress Center in Dresden, Germany.

The conference addresses all aspects of research into technologies for electronic and embedded systems engineering. An important part of the conference  is devoted to modeling, analysis, design and deployment of embedded software.

We invite you to submit papers to Topic E3: Model-based Design and Verification for Embedded Systems.

Main topics of interest:

Verification techniques for embedded and cyber-physical systems ranging from simulation, testing, model-checking, SAT and SMT-based reasoning, compositional analysis and analytical methods. Modeling, analysis and optimization of non-functional and performance aspects such as timing, memory usage, QoS and reliability. Model-based design of software architectures and deployment. Theories, languages and tools supporting model-based design flows covering software, control and physical components. Monitoring and run-time verification of embedded systems.

Topic Chair: Petru Eles, Linköping University, SE
Topic Co-Chair: Borzoo Bonakdarpour, University of Waterloo, CA,

Topic Subcommittee Members:

  • Sudipta Chattopadhyay, Singapore University of Technology and Design (SUTD), SG
  • Ylies Falcone, University Grenoble Alpes, FR
  • Florence Maraninchi, Verimag, FR
  • Kristin Rozier, Iowa State University, US
  • Lothar Thiele, ETH Zurich, CH

Please note:

Jul 172017

The paper entitled GREP: Games for the Runtime Enforcement of Properties has been accepted for publication in the proceedings of ICTSS 2017, the 29th IFIP International Conference on Testing Software and Systems.

Below is an abstract of the paper:

We present GREP, a tool for the runtime enforcement of (timed) properties. GREP takes an execution sequence as input (stdin), and modifies it (stdout) as necessary to enforce the desired property, when possible. GREP can enforce any regular timed property described by a deterministic and complete Timed Automaton. The main novelties of GREP are twofold: it uses game theory to improve the synthesis of enforcement mechanisms, and it accounts for uncontrollable events, i.e. events that cannot be controlled by the enforcement mechanisms and thus have to be released immediately. We present an overview of GREP and validate its usability with a performance evaluation.

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

The pre-print of the paper can be downloaded here.

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).