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.

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

Jun 112014
 

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.

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

 

May 062014
 

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.

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

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

Mar 242014
 

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.

Mar 112014
 

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.

Mar 102014
 

This week I am visiting HUST – Hanoi University of Sciences and Technology (aka IPH – Institut Polytechnique de Hanoi) to work with Thanh Hung Nguyen.

Feb 122014
 
PERSYVAL-Lab and NASA-JPL are organizing the second edition of the CPS Summer School. The broad objective of the CPS Summer School is to explore the manifold relationship between networked embedded systems (« the internet of things ») and humans as their creators, users, and subjects. The format of the Summer School is a five days meeting, organized around different aspects of rigorous engineering of Cyber-Physical Systems.

This year, the objective of the school is to survey fundamental and applied aspects of modelling, monitoring and learning of systems as well as to identify novel opportunities and research directions in these areas through a series of lectures by international experts. Participants will also experience the relevant technologies during hands-on courses and be given a chance to present their own work. The school will provide a great opportunity to know other people working in the field, to meet distinguished scholars, and to establish contacts that may lead to research collaborations in the future.

The school will concentrate on the fields of system modelling, monitoring and learning. Over the last ten years we have seen a lot of growth in these areas, building on strong theoretical foundations to apply and extend techniques to new application domains. Runtime verification is a growing field with more and more efffective applications in safety/mission-critical systems, enterprise and systems software, autonomous and reactive control systems, health management and diagnosis systems, and system security and privacy. The field of specification mining (learning specifications from system behaviour) has also seen a surge in research effort, with the establishment of a number of competitions to drive forward the development of practical tools. This research community is at an ideal stage to benefit from a school such as this, to inspire, motivate and instruct new researchers into the field.

Students participating at this summer school will learn the current state of the art in modeling, monitoring, and learning. Students will be able to apply new techniques coming from various communities and backgrounds to their own domain. The CPS Summer School will be held at Grenoble University. Courses will be given in English by experts from industry and academia working in various fields of CPS.

Topics:

• System modeling.
• Monitoring.
• Learning.
• Medical devices.
• Sensor networks.

Confirmed Speakers:

• Eric Bodden (TU Darmstadt and EC SPRIDE, Germany).
• Olivier Coutelou (Schneider Electric, France).
• Radu Grosu (Technical Univesity Wien, Austria).
• Jean Goubault-Larrecq (ENS Cachan, France).
• Klaus Havelund (NASA JPL, USA).
• Kim G. Larsen (Aalborg University, Denmark).
• Martin Leucker (University of Lübeck, Germany).
• Roberto Passerone (Universita’ degli Studi di Trento, Italy).
• Grigore Rosu (University of Illinois at Urbana Champaign, USA).
• Mohamad Sawan (Ecole Polytechnique de Montréal, Canada).
• Bernhard Steffen (Technical University Dortmund, Germany).
• Andreas Zeller (Saarland University, Germany).

Organization Committee:

• Saddek Bensalem – University of Grenoble, France.
• Yliès Falcone – University of Grenoble, France.
• Klaus Havelund – NASA JPL, USA.

Registration fee is €250 for students, €400 for non-students, which includes lunches and coffee breaks from Monday 8th through Thursday 11th, and a party. The registration fee only partially covers the costs incurred. The remaining costs are covered by PERSYVAL-Lab. The local organization committee has arranged university accommodations for students. Please refer to the Website for more details.

Application Procedure and Important Dates (please refer to the Website for the full procedure):

• Deadline for Application: April 14, 2014.
• Response to Applicants: April 21, 2014.
• Online Registration and Fee payment: May 10, 2014.
• Summer school on CPS: July 7-11, 2014.
Since attendance is limited, priority will be given to Ph.D. students and companies’ staff.More details can be found at: https://persyval-lab.org/en/summer-school/cps14.

Applications can be submitted at: https://persyval-calls.imag.fr/en/project/10.

Enquiries can be sent to cps-school.organization@imag.fr.