9:30 - 10:00 : Accueil, café / Welcome coffee. (room C48)

10:00 - 11:15 Session 1 MTV2 (in French) (room C48)

• Pamela CARVALLO (Télécom SudParis, SAMOVAR). Sécurité dans le cloud : Framework de détection de menaces internes basé sur l'analyse d'anomalies.
• Hai Nguyen Van (LRI). Sémantiques pour la synchronisation de systèmes polychrones et polytemporisés.
• Sarah Dahab (Télécom SudParis, SAMOVAR). Formal automated software measurement plan.
  [slides]

10:00 - 11:15 Session 2 MFDL (in French) (room C47)

• Aymerick Savary (LACL). Quand les modèles d’exigences et formels se rencontrent.
• Steve Jeffrey Tueno Fotso (LACL). Vers l'Utilisation d'Ontologies pour la Modélisation du Domaine au sein de la Méthode SysML/KAOS.
  [slides]
• Georges Ouffoué (LRI). How software applications can be tolerant to intruders through diversification and reflection?
  [slides]

11:15 - 11:40 Pause / Break. (room C48)

11:40 - 12:30 Session 3. Exposé invité industriel / Industrial Keynote. (room C48)

• Yves Génevaux (Argosim). Debug Textual Requirements and Automate Functional Tests of Embedded Systems.
  [slides]

12:30 - 14:00 Déjeuner / Lunch.

14:00 - 14:50 Session 4. Exposé invité / Keynote. (in English). (room C48)

• Rob Hierons (Brunel University London, UK). Optimal Product Selection from Feature Models.
  [slides]

14:50 - 15:15 Pause / Break. (room C48)

15:15 - 16:30 Session 5. (in English). (room C48)

• Yliès Falcone (Univ. Grenoble-Alpes / LIG). Monitoring Decentralized Specifications.
  [slides]
• Hélène Waeselynck (LAAS-CNRS). Can robot navigation bugs be found in simulation? An exploratory study.
• Maxime Puys (Univ. Grenoble-Alpes / VERIMAG). Generation of Applicative Attacks Scenarios Against Industrial Systems.
  [slides]

16:30 - 16:45 Annonces. Fin de la journée. / Announcements. Closing. (room C48)

Deux présentations invitées sont prévues

• Rob Hierons (Brunel University London, UK) : Optimal Product Selection from Feature Models
  A feature model specifies the sets of features that define valid products in a software product line. This talk explores the many-objective optimisation problem of choosing optimal products from a feature model based on user preferences. This problem has been found to be difficult for a purely search-based approach, leading to classical many-objective optimisation algorithms being enhanced by either adding in a valid product as a seed or by introducing additional mutation and replacement operators that use a SAT solver. This talk will describe the recently developed SIP method that instead enhances the search in two ways: by providing a novel representation and also by optimising first on the number of constraints that hold and only then on the other objectives.


• Yves Génevaux (Argosim) : Debug Textual Requirements and Automate Functional Tests of Embedded Systems
  Over the last two decades, there has been a real movement towards Requirements Engineering. Various tools that have been developed but they mostly focus on the requirements management and traceability, there was requirements validation tool available for checking their correctness. As a result, over half of the faults detected during the testing phases result from specification mistakes. This is particularly prejudicial in the case of critical embedded systems where specifications play a central role in the certification process
  Argosim STIMULUS provides an innovative solution for the verification of functional requirements during the specification phase. STIMULUS unique editing, debugging and simulation features enables the user to incrementally develop a specification based on textual requirements. System Architects can also verify if the specification they have developed meets the Safety Requirements. Later on, when a design model has been created, or a piece of code has been written, Test Engineers can automatically verify that the actual system meets its specification, including the Safety Requirements.
  This breakthrough has become possible as Stimulus relies on a high-level, constraint-based, textual language to express requirements that are very close to the natural language and a simulation engine based on a constraint solver to generate and analyze execution traces of the specified system. Visualizing "what" the specified systems will do enables system architects to discover incorrect, ambiguous, missing and conflicting requirements. The combination of ease of use and automation brought by STIMULUS changes radically the Requirement Engineering domain. (Authors: Fabien Gaucher and Yves Génevaux.)

The ability to navigate in diverse and previously unknown environments is a critical service of autonomous robots. The validation of the navigation software typically involves test campaigns in the field, which are costly and potentially risky for the robot itself or its environment. An alternative approach is to perform simulation-based testing, by immersing the software in virtual worlds. A question is then whether the bugs revealed in real worlds can also be found in simulation. The paper reports on an exploratory study of bugs in an academic software for outdoor robots navigation. The detailed analysis of the triggers and effects of these bugs shows that most of them can be revealed in low-fidelity simulation. It also provides insights into interesting navigation scenarios to test as well as into how to address the test oracle problem.

L'intégration de composants dans un système peut s'avérer difficile lorsque ces composants - qui utilisent des notions de temps différentes - doivent être synchronisés. Cette synchronisation peut être dirigée par les évènements (un évènement est provoqué par un autre), ou dirigée par le temps (un évènement se produit parce qu'il en est l'heure). De plus, différents composants peuvent utiliser différentes échelles de temps, ce qui rend l'utilisation d'une ligne detemps globale et unique impossible.
Nous nous intéressons à la spécification de schémas de synchronisation pour de tels systèmes polychrones et polytemporisés, et avons implémenté un modèle d'évènements discrets temporisé dans le langage TESL, qui est utilisé pour coordonner la simulation de modèles composites et pour tester l'intégration de systèmes.
Nous avons défini une sémantique dénotationnelle de TESL afin de nous assurer par construction de sa cohérence. Afin de pouvoir dériver des traces d'exécutions satisfaisant une spécification TESL, nous avons également développé une sémantique opérationnelle, ce qui introduit un risque d'incohérence entre les deux sémantiques. Pour éliminer ce risque, nous utilisons une sémantique intermédiaire coinductive reliant les sémantiques dénotationelle et opérationelle. Ces modèles sémantiques sont formalisés dans l'assistant de preuve Isabelle/HOL, ainsi que les preuves formelles assurant la correction, la complétude, le progrès et la terminaison locale.

Due to the complexity of the current software, the measurement processes become crucial activities. However, due to the quantity of aspects to be measured and the big amount of data to manipulate, the software measurement plans are heavy and costly to manage. It leads to very complex measurement plans engendering eventual losses of time and performance. In addition, to ensure a quality evaluation, a rigorous specification of the measurement plan is required especially for both design and integration phases of the evaluation plan. The main objectives of this presentation are to depict improvements for measurement plans management by formalizing our metrics with the OMG standard SMM, and making the metrics use more flexible. This allows to tackle specific useful metrics in avoiding measures that are not always relevant during an identified measured period of time. We propose to analyze and classify the measurements at runtime using a learning approach (Support Vector M achine, SVM) in order to define the relevant metrics that should be used during a specific duration. We designed a suggestion process that selects metrics from a current measurement plan or reorient (suggest) that measurement plan by proposing to execute other metrics. We implemented our framework on an industrial platform and successfully ran several experiments.

We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of the entire system. To do so, our approach introduces a data-structure that i) keeps track of the execution of an automaton, ii) has predictable parameters and size, and iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study decentralized monitorability, and present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Lastly, we introduce the THEMIS tool, which is a framework for designing such decentralized algorithms, and simulating their behavior.

THEMIS can be downloaded at: https://gitlab.inria.fr/monitoring/themis.

A demonstration of THEMIS is available at: https://gitlab.inria.fr/monitoring/themis-demo.

Dans cette recherche, nous proposons d’établir des liens entre un modèle d’exigences et un modèle formel qui permet de vérifier des propriétés sur ces exigences. Pour cela, nous proposons une méthode, basée sur des techniques de fédération de modèles, permettant de définir et de manipuler des liens de traçabilité entre ces deux modèles. Cette méthode est en cours de construction et une première implémentation, basée sur le logiciel OpenFlexo, a été réalisée. Pour les exigences, nous utilisons la méthode SysMLKaos. Celle-ci permet de lier logiquement des exigences entre elles et de les raffiner. Pour la partie formelle, nous reprenons les notations du langage Event-B et nous avons adapté la génération d’obligations de preuves afin qu’elles correspondent à la représentation d'exigences. Un métamodèle de ce langage a été proposé. Chacune de ces spécifications est représentée indépendamment dans OpenFlexo afin de les rendre disponibles pour d'autres projets. Pour fédérer ces deux modèles, et ainsi représenter nos liens de traçabilité, un troisième modèle est proposé. Ce dernier permet au travers de concepts fédérateurs d'établir des liens dynamiquement entre les deux représentations. Il permet ainsi d'encoder le sens d'une fédération et en cas de modification d'un des 2 modèles de pouvoir plus facilement le réparer.

Cloud Computing (CC) opens new possibilities for more flexible and efficient services for Cloud Service Clients (CSCs). However, one of the main issues while migrating to the cloud is that what it once was a private domain for CSCs, now is handled by a third-party, hence subject to their security policies. Therefore, CSCs' availability, confidentiality and integrity should be ensure. Although the existence of protection mechanisms, such as encryption, the monitoring of these properties becomes necessary. Additionally, new threats emerge everyday, which requires more efficient detection techniques.
The work presented in this document goes beyond the state of the art by treating the malicious insider threat, one of the least studied threats in CC. This is mainly due to the organizational and legal barriers from the industry, and therefore the lack of appropriate datasets for detecting it. We tackle this matter by addressing two challenges.
First, the derivation of an extensible methodology for modeling the behavior of a user in a company. This abstraction of an employee includes inter and intra psychological factors, contextual information and based in a role-based approach. The behaviors follow a probabilistic procedure, where the motivational malevolent motives are considered to occur with a given probability in time.
Second, the design and implementation of an anomaly-based detection framework for the aforementioned threat. This implementation enriches itself by comparing two different points of data capture: a profile-based view from the local network of the company, and a cloud-end view that analyses data from the services with whom the clients interact. This allows the learning process of anomalies to benefit from two perspectives: (1) the study of both real and simulated traffic with respect to the cloud service's interaction, in favor of the characterization of anomalies; and (2) the analysis of the cloud service in order to aggregate statistics that support the overall behavior characterization.
By using this framework, the main objective is to derive a technique capable of detecting a broader set of anomalies of the company's interaction with the cloud. This will be possible due to the replicable and extensible nature of the mentioned model. By taking advantage of the autonomic nature of machine learning techniques, we aim to consistently ensure the detection's performance for threat scenarios where the attack comes from inside the enterprise's assets.

In the context of security, risk analyzes are widely recognized as essential. However, such analyzes need to be replayed frequently to take into account new vulnerabilities, new protections, etc.. As exploits can now easily be found on internet, allowing a wide range of possible intruders with various capacities, motivations and resources. In particular in the case of industrial control systems (also called SCADA) that interact with the physical world, any breach can lead to disasters for humans and the environment. Alongside of classical security properties such as secrecy or authentication, SCADA must ensure safety properties relative to the industrial process they control. In this paper, we propose an approach to assess the security of industrial systems. This approach aims to find applicative attacks taking into account various parameters such as the behavior of the process, the safety properties that must be ensured. We also model the possible positions and capacities of attackers allowing a precise control of these attackers. We instrument our approach using the well known model-checker UPPAAL, we apply it on a case study and show how variations of properties, network topologies, and attacker models can drastically change the obtained results.

Software-based systems are nowadays complex and highly distributed. The efforts and findings of the last decades of research on the formalization and the verification of software have given a certain level of assurance on software applications. However new challenges such as high availability and security issues are not fully addressed. In fact, software applications (Web services, cloud applications, on premises applications) are exposed to attacks that appear continuously. In contrast, existing intrusion detection mechanisms are not always suitable for protecting these applications against new and sophisticated attacks that increasingly appear. These issues have naturally paved the way to a new research topic that aims at providing new techniques for making software applications attack tolerant. In this talk, for enabling attack tolerance in software applications, we will present our contribution which is a combination of techniques(monitoring, modeling) leveraging in particular diversification that is the quality or state of having many different forms, types, ideas, etc. Our intuition lays on the fact that having diverse layers and points of failure increase the security as it allows tolerance to a greater variety of attacks. Our second contribution is attack tolerance through software reflection. As some software applications must dynamically adapt their behavior at run-time in response to response to attacks, our solution aims at handling these changes and ensure that the system continues to work after the adaptation process and before the propagation of the attacks. Finally, we will conclude the talk with our results and a discussion to highlight the perspectives and research direction of our ongoing work.

L'ingénierie des exigences est la partie du génie logiciel qui s'intéresse aux activités d'élicitation, d'analyse, de spécification et de validation des exigences relatives à un système à mettre en place, activités qui constituent la pierre angulaire de tout projet de développement logiciel. L'occurrence de défaillances au cours de l'une de ces étapes est très souvent à l'origine de conséquences extrêmement désastreuses. Le projet FOMOSE, financé par l'Agence Nationale de la Recherche, vient en réponse à cette problématique et s'intéresse à l'élaboration de méthodes et d'outils pour la modélisation et la validation formelle des exigences de systèmes critiques et complexes. Dans le cadre de ce projet, la méthode SysML/KAOS a été proposée pour la modélisation des exigences fonctionnelles et non fonctionnelles sous la forme d'hiérarchies de buts. Afin de valider formellement ces exigences, une correspondance a été établie entre SysML/KAOS et la méthode formelle Event-B, ceci afin de produire des spécifications formelles à partir de modèles de buts. Malheureusement, la spécification formelle obtenue est incomplète : il est nécessaire de fournir manuellement la partie structurelle des machines Event-B et le corps des évènements. Au vu du fait que cette partie structurelle, composée des ensembles, des constantes, des propriétés, des variables et des axiomes du modèle formel, constitue une description des propriétés du domaine d'application du système, nous nous intéressons à une approche permettant de construire un modèle du domaine qui complémentera SysML/KAOS.

De l'état de l'art sur le sujet, il ressort que les ontologies constituent la forme par excellence de représentation de la connaissance d'un domaine du fait de leur richesse sémantique et de leur aspect formel. De plus, deux formalismes d'expression d'ontologies semblent le mieux s'arrimer à nos critères : OWL (Ontology Web Language) et PLIB (Part Library). Malheureusement, aucun d'eux ne permet de modéliser des connaissances dynamiques (connaissances susceptibles d'évoluer avec le temps). Nous nous proposons donc d'élaborer un nouveau formalisme de modélisation d'ontologies, fondée sur OWL et PLIB, et nous nous intéressons aux liens de correspondance entre ce formalisme et Event-B, ceci afin d'être capable de produire automatiquement la partie structurelle des spécifications formelles issues des modèles de buts SysML/KAOS à partir des ontologies.

Notre exposé consistera en une présentation du contexte sous-tendant notre étude, de l'état de l'art sur la modélisation du domaine, du formalisme que nous proposons pour la modélisation du domaine sous forme d'ontologies et des liens de correspondance entre ce formalisme et Event-B, tout ceci illustré au travers d'un cas d'étude traitant du système de contrôle de l'extension et de la rétraction du train d'atterrissage d'un avion.