Jan 042015
 

Tomorrow, I wil start a 2-week series of lectures at CETIC (the African Center of Excellence in computer science), Yaounde, Cameroon.

The subjects of the lecture are the semantics of programming languages and the design of compilers. It is based on the lecture given at Univ. Grenoble Alpes in the international master, but more practice oriented. In particular, the students will have to design a mini-compiler.

Many thanks to Prof. Maurice Tchuenté for the invitation.

Many thanks to Prof. Georges Kouamou, Prof. Jacques Tagoudjeu, and Prof. Maurice Tchuenté for the warm welcome.

Thanks to Inria for the support

logo         logo-inria

Dec 172014
 

Today is officially the first day of the COST Action Runtime Verification beyond Monitoring (ARVI).

A meeting of the Management Committee (MC) will be held in COST offices in Belgium.

I am representing France in the MC.

Below is a description of the COST action:

Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications.
There is a great potential applicability of RV beyond software reliability, if one allows monitors to interact back with the observed system, and generalizes to new domains beyond computers programs (like hardware, devices, cloud computing and even human centric systems). Given the European leadership in computer based industries, novel applications of RV to these areas can have an enormous impact in terms of the new class of designs enabled and their reliability and cost effectiveness.

EU COST Action IC1402 — project overview at the EU web-site.

cropped-Logo_cost-arvi_transp

Dec 152014
 

Runtime Verification is a verification technique for the analysis of software at execution-time based on extracting information from a running system and checking if the observed behaviors satisfy or violate the properties of interest. During the last decade, many important tools and techniques have been developed and successfully employed. However, there is a pressing need to compare such tools and techniques, since we currently lack a common benchmark suite as well as scientific evaluation methods to validate and test new prototype runtime verification tools.

The main aims of CRV-2015 are to:

  • Stimulate the development of new efficient and practical runtime verification tools and the maintenance and improvement of the already developed ones.
  • Produce a benchmark suite for runtime verification tools, by sharing case studies and programs that researchers and developers can use in the future to test and to validate their prototypes.
  • Discuss the metrics employed for comparing the tools.
  • Provide a comparison of the tools on different benchmarks and evaluate them using different criteria.
  • Enhance the visibility of presented tools among the different communities (verification, software engineering, cloud computing and security) involved in software monitoring.

CRV-2015 Organizers

Please direct any enquiries to the competition co-organizers (crv15.chairs _AT_ imag _DOT_ fr)

Yliès Falcone (Université Joseph Fourier, France).
Dejan Nickovic (AIT Austrian Institute of Technology GmbH, Austria).
Giles Reger (University of Manchester, UK).
Daniel Thoma (University of Luebeck, Germany).

CRV-2015 Jury

The CSRV Jury will include a representative for each participating team and the competition chairs. The Jury will be consulted at each stage of the competition to ensure that the rules set by the competition chairs are fair and reasonable.

Call for Participation

The main goal of CRV 2015 is to compare tools for runtime verification. We invite and encourage the participation with benchmarks and tools for the competition.The competition will consist of three main tracks based on the input language used:

  • Track on monitoring Java programs (online monitoring).
  • Track on monitoring C programs (online monitoring).
  • Track on monitoring of traces (offline monitoring).

The competition will follow three phases:

Benchmarks/Specification collection phase – the participants are invited to submit their benchmarks (C or Java programs and/or traces). The organizers will collect them in a common repository (publicly available). The participants will then train their tools using the shared benchmarks.
Monitor collection phase – the participants are invited to submit their monitors. The participants with the tools/monitors that meet the qualification requirements will be qualified for the evaluation phase.
Evaluation phase – the qualified tools will be evaluated on the submitted benchmarks and they will be ranked using different criteria (i.e., memory utilization, CPU utilization, …). The final results will be presented at the RV 2015 conference.

More information is available at: http://rv2015.conf.tuwien.ac.at/?page_id=276

Nov 272014
 

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.

Oct 032014
 

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.

Sep 222014
 

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

Sep 012014
 

NFM 2015

April 27-29, 2015, Pasadena, California, USA
Submission deadline: November 10, 2014

NFM15_small

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:

lncsSpringer_Logo