The paper Enforcement and Validation (at runtime) of Various Notions of Opacity has been accepted to Discrete Event Dynamic Systems, a Springer journal. This is an extended version of our paper that appeared in CDC 2013. One of the new contributions of this paper is to introduce what we call K-step strong opacity. The abstract of the paper […]
Category: papers
Efficient and Generalized Decentralized Monitoring of Regular Languages
The paper Efficient and Generalized Decentralized Monitoring of Regular Languages has been accepted to FORTE’14, the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems, June 3-6, 2014, Berlin, Germany. Below is the abstract of the paper. This paper proposes an efficient and generalized decentralized monitoring algorithm allowing to detect satisfaction or violation of […]
Runtime Enforcement of Regular Timed Properties
The paper Runtime Enforcement of Regular Timed Properties is accepted to the ACM Symposium on Applied Computing, Software Verification and Testing Track, Gyeongju, Korea, March 24 – 28, 2014. Runtime enforcement is a verification/validation technique aiming at correcting (possibly incorrect) executions of a system of interest. In this paper, we consider enforcement monitoring for systems with timing specifications (modeled […]
Fault Localization in Embedded Software based on a Single Cyclic Trace
The paper Fault Localization in Embedded Software based on a Single Cyclic Trace has been accepted to ISSRE 2013, the 24th IEEE International Symposium on Software Reliability Engineering, Pasadena, CA. Locating faults in embedded software, especially in microcontroller context, is still difficult. Quite recently, it became possible to recover execution traces from microcontrollers using specific hardware probes. However, […]
Runtime Enforcement of K-step Opacity
The paper Runtime Enforcement of K-step Opacity has been accepted to CDC, 52nd IEEE Conference on Decision and Control that will be held Tuesday through Friday, December 10-13, 2013 at Palazzo dei Congressi, Florence, Italy. We study the enforcement of K-step opacity at runtime. In K-step opacity, the knowledge of the secret is of interest to the attacker within K […]
Runtime Verification of Component-Based Systems in the BIP Framework with Formally-Proved Sound and Complete Instrumentation
The paper Runtime Verification of Component-Based Systems in the BIP Framework with Formally-Proved Sound and Complete Instrumentation has been accepted to the international journal SOSYM: SOftware and SYstem Modeling. Here is an abstract of the paper: Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact […]
Best Paper Award at FM’12
On August 30, we have received the Best Paper Award from Formal Methods Europe and the PC of FM’2012, the 18th international symposium on Formal Methods. This award comes for our paper Decentralised LTL Monitoring.
Runtime Enforcement of Timed Properties
The paper Runtime Enforcement of Timed Properties has been accepted for publication at the conference RV’12: 3rd international conference on Runtime Verification, Istanbul, Turkey. Here is an abstract of this paper below: Runtime enforcement is a powerful technique to ensure that a running system respects some desired properties. Using an enforcement monitor, an (untrusted) input […]
More Testable Properties
The journal paper More Testable Properties has been recently accepted for publication in the journal Software Tools for Technology Transfer. This paper is joint work with my friends and colleagues from Verimag (Jean-Claude Fernandez and Laurent Mounier) and from Inria Rennes – Bretagne Atlantique (Thierry Jéron and Hervé Marchand). The paper shall appear in STTT […]