International audience

Cyber-Physical Systems (CPS) contain complex computational components that control physical entities.The design of these components must take into account the realtime and concurrent nature of these systems.Formulating requirements that describe CPS behaviors precisely, ruling out misunderstandings, is a crucial yet difficult endeavor.To increase trust in the requirements, formal methods can be used to check relevant properties of the requirements.We investigate a process algebra to capture real-time behaviors and concurrency in CPS requirements in order to automate their analysis.We use a structured natural language to first express CPS requirements: this takes into account current practice, indeed requirements should be easily writable as well as graspable by stakeholders with various points of view and ease communication among them.At the same time, requirements analysis using simulation or formal validation is possible by taking advantage of the requirements structure.We discuss translation from the structured requirements into the process algebra to automate the overall process.Our approach is implemented and is illustrated by an example issued from CPS4EU project 1 .

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route. Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in NPTIME) whether there exists a network topology that would allow malicious nodes to mount an attack against the protocol, for a bounded number of sessions. We also provide a decision procedure for detecting attacks in case the network topology is given a priori. We demonstrate the usage and usefulness of our approach by analyzing the protocol SRP applied to DSR.