The paper Runtime Enforcement for Component-Based Systems has been accepted for publication in SAC-SVT 2015, the 30th ACM/SIGAPP Symposium On Applied Computing – Software Verification and Testing track, Salamanca, Spain.

Here is the abstract of the paper.

We propose a theoretical runtime enforcement framework for component-based systems (CBS) where we delineate a hierarchy of enforceable properties (i.e., properties that can be enforced) according to the number of observational steps a system is allowed to deviate from the property (i.e., the notion of k-step enforceability). To ensure the observational equivalence between the correct executions of the initial system and the monitored system, we show that i) only stutter-invariant properties should be enforced on CBS with our monitors, ii) safety properties are $1$-step enforceable. Given an abstract enforcement monitor for some 1-step enforceable property, we formally instrument (at relevant locations) a system to integrate the monitor. At runtime, the monitor observes and automatically avoids any error in the behavior of the system w.r.t. the property.

This is joint work with H. Charafedine, K. El-Harake, and M. Jaber.

The paper Runtime Enforcement of Timed Properties Revisited has been accepted for publication in Formal Methods in System Design, a Springer journal. Below is the abstract of the paper.

Runtime enforcement is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties.

This paper deals with runtime enforcement of timed properties by revisiting the foundations of runtime enforcement when time between events matters. We propose a new enforcement paradigm where enforcement mechanisms are time retardants: to produce a correct output sequence, additional delays are introduced between the events of the input sequence. We consider runtime enforcement of any regular timed property defined by a timed automaton. We prove the correctness of enforcement mechanisms and prove that they enjoy two usually expected features, revisited here in the context of timed properties. The first one is soundness meaning that the output sequences (eventually) satisfy the required property. The second one is transparency, meaning that input sequences are modified in a minimal way. We also introduce two new features, i) physical constraints that describe how a time retardant is physically constrained when delaying a sequence of timed events, and ii) \emph{optimality}, meaning that output sequences are produced as soon as possible. To facilitate the adoption and implementation of enforcement mechanisms, we describe them at several complementary abstraction levels. Our enforcement mechanisms have been implemented and our experimental results demonstrate the feasibility of runtime enforcement in a timed context and the effectiveness of the mechanisms.

Keywords: runtime verification, runtime enforcement, timed properties, timed automata, software engineering.

This is joint work with S. Pinisetty, T. Jéron, H. Marchand, A. Rollet, and O. Nguena-Timo.

This week I am attending RV 2014, the 14th International Conference on Runtime Verification, September 22 – September 25, 2014 Toronto, Canada.

In addition to enjoying the nice talks from the RV community, I will present the current status of CSRV 2014, the first international Competition on Software for Runtime Verification that I am co-chairing with E. Bartocci and B. Bonakdarpour.

C. Colombo will also present our paper Organising LTL Monitors over Distributed Systems with a Global Clock (preprint).

NFM 2015

April 27-29, 2015, Pasadena, California, USA

The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.

Topics of interest

Symposium topics of interest include but are not limited to the following:

• Model checking
• Theorem proving
• SAT and SMT solving
• Symbolic execution
• Static analysis
• Runtime verification
• Program refinement
• Compositional verification
• Security and intrusion detection
• Modeling and specification formalisms
• Model-based development
• Model-based testing
• Requirement engineering
• Formal approaches to fault tolerance
• Applications of formal methods to aerospace systems
• Applications of formal methods to cyber-physical systems
• Applications of formal methods to human-machine interaction analysis

Registration

There will not be a registration fee charged to participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register. The registration website will be activated closer to the event.

Organization

NFM 2015 is organized by Laboratory for Reliable Software (LaRS) at NASA’s Jet Propulsion Laboratory (JPL). JPL is a federally funded research and development center and NASA field center, managed by the nearby California Institute of Technology (Caltech) for the National Aeronautics and Space Administration. The laboratory’s primary function is the construction and operation of planetary robots and spacecraft, for example the Mars rovers.

NFM 2015 is the seventh edition of the NASA Formal Methods Symposium, steered by the NASA Formal Methods Group.  The symposium grew out of a workshop series started by the NASA Langley Formal Methods Group, and is now held annually, hosted each year by one of the NASA centers.

Proceedings to be published in:

The paper Organising LTL Monitors over Distributed Systems with a Global Clock has been accepted in RV 2014: the 14th International Conference on Runtime Verification, September 22 – September 25, 2014 Toronto, Canada.

Here is the abstract of the paper:

Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system, allowing them to directly specify correctness properties on the global system behaviour. To support this abstraction, a compilation of the properties would not only involve the typical choice of monitoring algorithm, but also the organisation of submonitors across the component network. Existing approaches, considered in the context of LTL properties over distributed systems with a global clock, include the so-called orchestration and migration approaches. In the orchestration approach, a central monitor receives the events from all subsystems. In the migration approach, LTL formulae transfer themselves across subsystems to gather local information.

We propose a third way of organising submonitors: choreography — where monitors are orgnized as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise this approach, proving its correctness and worst case performance, and report on an empirical investigation comparing the three approaches on several concerns of decentralised monitoring.

This is joint work with Christian Colombo from University of Malta.

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 is below.

We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.

This is joint work with Hervé Marchand, from Inria Rennes.

ETAPS 14 starts in a week.

This week I am attending SAC 2014, the 29th Symposium On Applied Computing, Gyeongju, Korea. I am also presenting our work with Inria Rennes on Runtime Enforcement of Regular Timed Properties.

edit: Here are the slides I have presented.

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 any regular specification by local monitors alone in a system without central observation point. Our algorithm does not assume any form of synchronization between system events and communication of monitors, uses state machines as underlying mechanism for efficiency, and tries to keep the number and size of messages exchanged between monitors to a minimum. We provide a full implementation of the algorithm with an open-source benchmark to evaluate its efficiency in terms of number, size of exchanged messages, and delay induced by communication between monitors. Experimental results demonstrate the effectiveness of our algorithm which outperforms the previous most general one along several (new) monitoring metrics.

This is joint work with Tom Cornebize and Jean-Claude Fernandez, LIG and Verimag lab, Grenoble.