Publications

Internet est un système clé dans la société contemporaine. Il s'agit d'un système complexe réparti entre de nombreuses organisations ayant une variété de rôles et d'intérêts. Depuis leur création, les cyberattaques sont devenues des actifs précieux, car elles donnent aux rivaux des avantages, par exemple dans les domaines politique ou économique. Il est nécessaire d'analyser ces attaques, d'identifier leurs singularités et les mécanismes sur lesquels elles s'appuient afin de les contrer. Cela permettra d'établir des signatures plus précises et plus pertinentes et aidera la conception des contre-mesures. Un des aspects d'analyse des attaques sont les infrastructures utilisées par les attaquants pour générer les attaques. De nombreux outils aujourd'hui permettent de caractériser l'aspect technique des machines qui composent ces infrastructures. Mais comme les attaques ont lieu dans un environnement social, politique, économique et organisationnel, nous revendiquons qu'il est nécessaire d'évaluer ces machines d'un point de vue organisationnel. Cette thèse propose une méthodologie originale de catégorisation des adresses IP, à l'aide de 6 étiquettes décrivant deux axes : un axe technologique et un axe organisationnel. Nous proposons également un outil d'investigation, IPSeen, qui implémente cette méthodologie, en affectant les étiquettes aux adresses IP. Il s'appuie sur différentes sources de données : Wikidata, RDAP, Onyphe, GeoIPLite. Deux versions d'IPSeen sont proposées et évaluées dans ce manuscrit. Ces deux versions se différencient par leur rapidité et leur niveau de précision. Enfin, nous appliquons notre méthodologie à un ensemble de données réelles de suivi d'infrastructure de type 'command and control'. L'analyse produite propose une description des infrastructures des organisations qui administrent les machines participant aux infrastructures d'attaques. Nous montrons que notre approche apporte un éclairage essentiel sur la compréhension des attaques, en complément des nombreuses caractérisations techniques par ailleurs disponibles.

Keywords: Qualification des IPs, Sécurité, Réseaux, Métrologie

Crude oil leakages and spills (OLS) isare some of the problems attributed to pipeline failures in the oil and gas industry’s midstream sector. Consequently, they are monitored via several leakage detectiondetection and localisation techniques (LDTs) comprising classical methods and, recently, Internet of Things (IoT)-based systems via wireless sensor networks (WSNs). Although the latter techniques are proven to be more efficient, they are susceptible to other types of failures such as high false alarms or single point of failure (SPOF) due to their centralised implementations. Therefore, in this work, we present a hybrid distributed leakage detection and localisation technique (HyDiLLEch), which combines multiple classical LDTs. The technique is implemented in two versions, a single-hop and a double-hop version. The evaluation of the results is based on the resilience to SPOFs, the accuracy of detection and localisation, and communication efficiency. The results obtained from the placement strategy and the distributed spatial data correlation include increased sensitivity to leakage detection and localisation and the elimination of the SPOF related to the centralised LDTs by increasing the number of node-detecting and localising (NDL) leakages to four and six in the single-hop and double-hop versionversions, respectively. In addition, the accuracy of leakages is improved from 0 to 32 m in nodes that were physically close to the leakage points while keeping the communication overhead minimal.

Keywords: WSN; IoT-based monitoring systems; distributed systems; distributed leakage detection; distributed leakage localisation; crude oil pipelines

Le bon usage des outils numériques est indispensable pour garantir la fluidité et la sécurité des études, puis tout au long de la carrière de l'ingénieur·e. Dans le secondaire, les élèves ont accès pour partie à ces outils, entraînant à leur arrivée à l'INSA un sentiment de maîtrise suffisante, masquant leurs besoins réels et limitant leur motivation à progresser. Par conséquent, il apparaît un sentiment de désengagement d'une partie des enseignants pour s'impliquer dans la formation relative à ces outils. En effet, soit les enseignants considèrent qu'une formation spécifique au numérique est inutile car les étudiants savent déjà beaucoup de choses, soit que cette formation doit être dispensée par les seuls enseignants d'informatique, lesquels ne sont pas toujours motivés pour enseigner les outils logiciels qu'ils estiment en dehors de leur champ d'action.

Le module SOL, mis en place en 22-23 à l'INSA Lyon, est un module spécifiquement dédié au numérique avec la volonté de faire interagir des enseignants de toutes les disciplines du FIMI. Sa thématique va des outils de bureautique aux architectures matérielles en passant par l'hygiène numérique. Nous proposons ici de faire un retour d'expérience du montage de ce module en mettant en évidence les freins et leviers avec lesquels l'équipe a dû composer. La transdisciplinarité de son équipe pédagogique a permis une plus grande largeur de spectre des exercices abordés, et a pu faire émerger de nouvelles thématiques non identifiées à l'avance.

Pipeline failures in crude oil transportation occur due to ageing infrastructure, third-party interferences, equipment defects and naturally occurring failures. Consequently, hydrocarbons are released into the environment resulting in environmental pollution, ecological degradation, and unprecedented loss of lives and revenue. Hence, multiple leakage detection and monitoring systems (LDMS) are employed to mitigate such failures. More recently, these LDMS include Wireless Sensor Networks (WSN) and Internet of Things (IoT)-based systems. While they are proven more efficient than other LDMS, many challenges exist in adopting such systems for pipeline monitoring. These include fault tolerance, energy consumption, accuracy in leakage detection and localisation, and high false alarms, to cite a few. Therefore, our work seeks to address some challenges in implementing IoT-based systems for crude oil pipelines in a resilient end-to-end manner. Specifically, we consider the aspect of accurate leakage detection and localisation by introducing a unique node placement strategy based on fluid propagation for sensitive and multi-sized leakage detection. We also propose a new distributed leakage detection technique (HyDiLLEch) in the WSN layer. It is based on a fusion of existing leakage detection techniques such as the negative pressure wave method, gradient-based method, and pressure point analysis. With HyDiLLEch, we efficiently eliminate single points of failure. Furthermore, we implement fault-tolerant data and service management in the fog layer utilising the Nigerian National Petroleum Corporation (NNPC) pipeline network as a use case. The problem is modelled as a regionalised data-driven game against nature on the NNPC pipeline. Our proposed regionalised solution (R-MDP) using reinforcement learning optimises accuracy and fault tolerance while minimising energy consumption. Overall, our system guarantees resiliency to failures and efficiency in terms of detection and localisation accuracy and energy consumption.

Keywords: Informatics, IoT - Internet of Things, Wireless sensor network, Monitoring, Failure, Leak detection, Energy consumption, Pipelines, Distributed systems, Resilience, Reinforcement learning, Markov chains

There is a constant threat of having our computing systems under attack. Information regarding the origins of the traffic we receive can be valuable. Currently, the AS-number and the localization are the most commonly used IP-related information to characterize an attack.In this paper, we propose expanding knowledge about a remote IP’s owner to improve defensive reaction effectiveness and obtain in-depth analyzes of attacker profiles. We introduce the enrichment with socio-organizational information (such as organization type, activity field, etc.) about the entities owning the IP in addition to infrastructural information. This integration is driven by combining RDAP and Wikidata. We demonstrate that this proposal is promising.

Keywords: location awareness;network topology;semantics;europe;reinforcement learning;complexity theory;ip networks

One of the major failures attributed to pipeline transportation of crude oil is oil leakages and spills. Hence, it is monitored via several classical leak detection techniques (LDTs), which are more recently implemented on centralised wireless sensor networks (WSN)-based leak detection and monitoring systems (LDMS). However, the LDTs are sometimes prone to high false alarms, and the LDMS are sensitive to single points of failure. Thus, we propose HyDiLLEch, a distributed leakage detection and localisation technique based on a fusion of several LDTs. In this work, we implemented HyDiLLEch and compared it to the individual LDTs in terms of communication efficiency and leakage detection and localisation accuracy. With HyDiLLEch, the number of nodes detecting and localising leakages increases by a maximum of four to six times, thereby eliminating single points of failures. In addition, we improve the accuracy of localisation in nodes physically-close to the leak and maintain an average of 96% accuracy with little to no communication overhead.

Face au constat d’une hétérogénéité grandissante des savoir-faire et connaissances en informatique des étudiants à l'arrivée en première année, et le risque de son exacerbation dans le contexte du "nouveau bac", nous avons voulu expérimenter une approche pédagogique, qui permette une gestion de cette hétérogénéité tout en respectant les contraintes d'un emploi du temps homogène et un coût constant. Les actions menées s’articulent autour de 4 pôles : la constitution de groupes de niveau, avec une attention particulière portée sur les 2 niveaux extrêmes (renforcement et avancé/en autonomie), la mise en place de QCMs réguliers, l'utilisation ponctuelle de l'Apprentissage Par Problème (APP), et un auto-positionnement. L'expérimentation est encore en cours, mais déjà de premiers éléments permettent d'ouvrir les échanges.

Pipeline networks dominate the oil and gas mid-stream sector, and although the safest means of transportation for oil and gas products, they are susceptible to failures. These failures are due to manufacturing defects, environmental effects, material degradation, or third party interference through sabotage and vandalism. Internet of Things (IoT)-based solutions are promising to address these by monitoring and predicting failures. However, some challenges remain in the deployment of industrial IoT-based solutions, as the reliability, the robustness, the maintainability, the scalability, the energy consumption, etc. This paper is therefore aimed at highlighting potential solutions for detection and mitigation of pipeline failures while addressing the robustness, the cost and scalability issues of such approach efficiently across the network infrastructure, data and service layers.

La mise aux enchères des fréquences pour le déploiement de la 5G, à rebours des recommandations de la convention citoyenne sur le climat, a relancé un débat public sur l’impact énergétique des infrastructures numériques. Si ces infrastructures permettent d’optimiser notre consommation d’énergie, leur prolifération peut également produire l’effet inverse à celui escompté et finalement menacer la transition vers un modèle énergétique et sociétal « bas carbone ». De quelle manière peut-on conjuguer sobriété et numérique ?

La certification PIX remplacera le C2I (Certificat Informatique et Internet) à la rentrée 2019. Elle a d’ores et déjà été mise en place dans les INSA Rouen, Lyon et Rennes pour une partie des étudiants et le sera à l’INSA Strasbourg dès l’année 2020. Dans le cadre de cette communication, nous proposons de présenter l’intérêt d’accompagner nos étudiants dans l’acquisition d’une culture et de compétences numériques ainsi que les objectifs de cette certification, sa mise en œuvre et les premiers résultats.

This work addresses the problem of monitoring stateful services on a dynamic service-oriented architecture (SOA), such as OSGi. Indeed, in such architecture, services may disappear and appear, and if a used service disappears, then the client doesn't receive any notification. In such cases, classical monitoring approaches with statically linked monitors into services cannot be used. In this paper, we propose an OSGi based runtime monitoring system which enables to make security and self-healablility enforcement of dynamic services. For monitoring coherent stateful services usage, a transactional approach is defined to preserve the current run and collected data. In order to proof the validation of this solution, we give an implementation guidelines based on OSGi platform.

Keywords: Dynamic SOA, OSGi, runtime monitoring, service substitution, stale reference, transactional approach},

Cet article décrit un travail préliminaire autour du langage de programmation Golo. Notre objectif est de fournir aux développeurs des outils permettant de renforcer leur confiance en leur code. Pour ce faire, nous avons expérimenté plusieurs approches (test dynamique, analyse de type et preuve de programme) et nous cherchons maintenant des choix pertinents pour avancer dans chacune de ces pistes.

Keywords: Golo – typage – test – preuve.

L'ingénieur humaniste doit comprendre le monde et œuvrer à la diffusion large et sans barrières ni discrimination de la connaissance. Ce concept résonne largement avec celui de la culture libre, qui promeut la liberté de distribution des biens non matériels tels que logiciels, inventions, connaissances, etc.. Nous défendons donc dans cette communication que la sensibilisation à la culture libre est à la fois une opportunité et une nécessité pour la formation d'ingénieurs humanistes. Nous proposons également quelques pistes de réflexion pour l'intégration de cette culture libre dans notre contexte.

Keywords: Humanisme ; Culture libre

Dans le monde actuel, où la concentration est de plus en plus volatile, il devient important de permettre une meilleure immersion de l'apprenant afin d'exploiter son papillonnage dans le cadre de son apprentissage. Différentes démarches déjà. Dans cette communication, nous proposons une approche instrumentée numériquement, ayant pour but d'augmenter implication de l'apprenant. Si la réalité augmentée permet de superposer un monde virtuel par dessus la vision du monde réel, alors nous pourrions appeler enseignement augmenté un enseignement où l'étudiant a une interaction enrichie avec le monde réel.

Keywords: Numérique ; apprentissage ; interaction

The base motivation of Mobile Cloud Computing was empowering mobile devices by application offloading onto powerful cloud resources. However, this goal can't entirely be reached because of the high offloading cost imposed by the long physical distance between the mobile device and the cloud. To address this issue, we propose an application offloading onto a nearby mobile cloud composed of the mobile devices in the vicinity-a Spontaneous Proximity Cloud. We introduce our proposed dynamic, ant-inspired, bi-objective offloading middleware-ACOMMA, and explain its extension to perform a close mobile application offloading. With the learning-based offloading decision-making process of ACOMMA, combined to the collaborative resource sharing, the mobile devices can cooperate for decision cache sharing. We evaluate the performance of ACOMMA in collaborative mode with real benchmarks Face Recognition and Monte-Carlo algorithms-and achieve 50% execution time gain.

Keywords: Learned-based Decision-Making ; Mobile Cloud Computing ; Spontaneous Proximity Cloud ; Collaborative Application Offloading ; Resource Sharing ; Decision Cache ; Offloading Middleware

This paper won the Best Paper Award.

The explosive trend of smartphone usage as the most effective and convenient communication tools of human life in recent years make developers build ever more complex smartphone applications. Gaming, navigation, video editing, augmented reality, and speech recognition applications require considerable computational power and energy. Although smart- phones have a wide range of capabilities - GPS, WiFi, cameras - their inherent limitations - frequent disconnections, mobility - and significant constraints - size, lower weights, longer battery life - make difficult to exploiting their full potential to run complex applications. Several research works have proposed solutions in application offloading domain, but few ones concerning the highly changing properties of the environment. To address these issues, we realize an automated application offloading middleware, ACOMMA, with dynamic and re-adaptable decision-making engine. The decision engine of ACOMMA is based on an ant- inspired algorithm.

Keywords: Ant Colony Optimization ACO ; Mobile Cloud Computing ; Distributed systems ; Offload computing ; Spontaneous Proximity Cloud ; Decision-making algorithm ; Ant Algorithm

Easily programming behaviors is one major issue of a large and reconfigurable deployment in the Internet of Things. Such kind of devices often requires to externalize part of their behavior such as the sensing, the data aggregation or the code offloading. Most existing context-oriented programming languages integrate in the same class or close layers the whole behavior. We propose to abstract and separate the context tracking from the decision process, and to use event-based handlers to interconnect them. We keep a very easy declarative and non-layered programming model. We illustrate by defining an extension to Golo-a JVM-based dynamic language.

Keywords: Programming Language ; Context-Oriented Programming ; Decoupled Architecture ; Event-Based Handling ; JVM ; Golo.

Golo is a simple dynamically-typed language for the Java Virtual Machine. Initially implemented as a ahead-of-time compiler to JVM bytecode, it leverages invokedy-namic and JSR 292 method handles to implement a reasonably efficient runtime. Truffle is emerging as a framework for building interpreters for JVM languages with self-specializing AST nodes. Combined with the Graal compiler, Truffle offers a simple path towards writing efficient interpreters while keeping the engineering efforts balanced. The Golo project is interested in experimenting with a Truffle interpreter in the future, as it would provides interesting comparison elements between invokedynamic versus Truffle for building a language runtime.

Dans le cadre de la mise en place de l'évaluation des enseignements au premier cycle de l'INSA Lyon, le principal problème a été de permettre un passage à l'échelle de la démarche, tout en respectant le droit des enseignants à la confidentialité des résultats. Il était également nécessaire d'informer les étudiants et les collègues sur l'intérêt de la démarche, tout en sensibilisant dès le départ sur au temps nécessaire. Cependant, des problèmes demeurent et le groupe de travail continue ses réflexions et sa recherche d'outils pour progresser.

Mots clefs : Évaluation des enseignements -- Passage à l'échelle.

Taux de sélection : 50%

Formal methods are based on mathematical notations which allow to rigorously reason about a model and ensure its correctness by proofs and/or model-checking. Unfortunately, these notations are com- plex and often difficult to understand from a human point of view es- pecially for engineers who are not familiar with formal methods. Sev- eral research works have proposed tools to support formal models using graphical views. On the one hand, such views are useful to make for- mal documents accessible to humans, and on the other hand they ease the verification of some behavioral properties. However, links between graphical and formal models proposed by these approaches are often difficult to put into practice and depend on the targeted formal lan- guage. In this paper, we discuss these links from a practical approach and show how a behavioral description can be computed from a formal model based on two complementary paradigms: under-approximation (or animation-based) and over-approximation (or proof-based). We applied these paradigms in order to produce behavioural state/chart views from B models and we carried out an empirical study to assess the quality and relevance of these graphical representations for humans.

Keywords: B method, Symbolic LTS, Animation, Abstraction.

In the context of Dynamic Service-oriented Architecture(SOA), where services may dynamically appear or disappear transparently to the user, if a reference of disap- peared service is used by another service, classical monitoring systems can't deal with the use of such stale reference, even though the monitoring system has dynamicity resilience (i.e., OSGiLarva). In this paper, we propose a monitoring system, named NewMS, which has dynamicity resilience as well as capability of handling stale references without restarting monitored systems.

Keywords: Dynamic SOA; OSGi; Runtime Verification; Stale Reference; Service Substitution.

Dynamic service-oriented architectures (D-SOA) focus on loosely coupled client- server interactions where both of them can appear and disappear at runtime. Our goal is to design monitoring systems for these architectures. Since classical monitoring systems are statically injected into the monitored services, they cannot properly handle the runtime services’ lifecycle. Moreover, when a service is substituted by a new one, other services may still use the old reference. This reference is kept in memory as a stale reference which induces some forbidden behaviors. This thesis contributes to design a monitoring system with resilient dynamicity that monitors services usage and is able to deal with stale references usage. This goal is achieved in three steps. Firstly, by considering the dynamicity of SOA systems in an open environment, we design a corresponding dynamic monitoring approach. We identify two key properties of the loosely coupled monitoring system: dynamicity resilience, i.e., after the unregistration of a service, its interface monitor and its current state are kept alive in memory and transferred to a new loaded service; comprehensiveness, i.e., the implementations of the monitored interface can’t bypass the monitor observations. Secondly, to avoid stale references usage, we propose a client-side safe service usage (SSU) layer to automatically handle them. If a used service disappears, then the SSU layer can either transparently substitute it or throw an exception to the client. This SSU layer is based on a transactional approach which aims to preserve the coherence of active services. Thirdly, we propose to integrate both approaches into a new monitoring system (NewMS). The NewMS inherits the principles of both systems: dynamicity resilience, comprehensiveness and fault tolerant. It can dynamically monitor service usage and transparently handle stale references of dynamic SOA systems. All the three propositions are implemented on OSGi-based platform. We develop a simple application that simulates an Airline Reservation system, which is monitored by our monitoring systems. We also develop various automata to handle the dynamicity of the Airline Reservation system in the NewMS. Our results demonstrate that the time cost of our monitoring systems is close to one of classical monitoring systems.

Keywords: Information Technology, Dynamic ervices oriented architecture - D-SOA, Services use, Monitoring slip, Fault Tolerance, Stale reference

Architecture is an approach where software systems are designed in terms of a composition of services. OSGi is a Service-Oriented Framework dedicated to 24/7 Java systems. In this Service-Oriented Programming approach, software is composed of services that may dynami- cally appear or disappear. In such a case, classical monitoring approaches with statically injected monitors into services cannot be used. In this paper, we describe ongoing work proposing a dynamic monitoring approach dedicated to local SOA systems, focusing particularly on OSGi. Firstly, we define two key properties of loosely coupled monitoring systems: dynamicity resilience and comprehensiveness. Next, we propose the OSGiLarva tool, which is a preliminary implementation targeted at the OSGi framework. Finally, we present some quantitative results showing that a dynamic monitor based on dynamic proxies and another based on aspect-oriented programming have equivalent performances.

Keywords: Monitoring, Dynamic SOA, OSGi, Larva, LogOs.

In a model-based testing approach as well as for the verification of properties, B models provide an interesting modelling solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used. The abstraction is often a domain abstraction of the state variables that requires many proof obligations to be discharged, which can be very time consuming for real applications.

This paper presents a contribution to this problem that complements an approach based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a \B event model, in addition to three methods that choose relevant variables according to a test purpose. In this way, we propose a method that computes an abstraction of a source model m according to a set of selected relevant variables. Depending on the method used, the abstraction can be computed as a simulation or as a bisimulation of m. With this approach, the abstraction process produces a finite state system. We apply this abstraction computation to a Model Based Testing process. We evaluate experimentally the impact of the model simplification by variables elimination on the size of the models, on the number of proof obligations to discharge, on the precision of the abstraction and on the coverage achieved by the test generation.

Keywords: Abstraction, Test Generation, (Bi)Simulation and Slicing.

Taux de sélection : 44%

This paper introduces Golo, a simple dynamic programming language for the Java Virtual Machine (JVM) that has been designed to leverage the capabilities of the new Java 7 invokedynamic instruction and API (JSR 292). Golo has its own language constructs being designed with invokedynamic in mind, whereas existing dynamic languages for the JVM such as Groovy, JRuby or Nashorn have to adapt language constructions which are sometimes hard to optimize. Coupled with a minimal runtime that directly uses the Java SE API, Golo is an interesting language for rapid prototyping, polyglot application embedding, research (e.g., runtime extensions, language prototyping) and teaching (e.g., programming, dynamic language runtime implementation). We show that the language design around invokedynamic allows for a very concise runtime code base with performance figures that compare favorably against Java and other dynamic JVM languages. We also discuss its future directions, either as part of Golo or through language and runtime research extensions.

Keywords: Golo, invokedynamic, Java, JVM, languages, compilers

Internet of Things devices are physically closed to the end user but suffer from poor execution environments. By contrast, cloud computing provides effective virtualization of data and services, but without the user fine-grained context vision. We emphasize that next smartphone generations are the universal interface between these two worlds. Existing approaches generally use ad hoc architectures and a predefined execution environment and focus only on the optimization between the smartphone and the cloud. We propose a service-oriented middleware approach where smartphones are the gateway link between IoT and Cloud services.

Keywords: Cloud Computing; Internet of Things; Service-Oriented Applications; Smart and Autonomic Gateway; Smartphone

The service oriented approach is a paradigm allowing the introduction of dynamicity in developments. If there are many advantages with this approach, there are also some new problems associated to service disappearance. The particular case of service substitution is often studied and many propositions exist. However, proposed solutions are mainly server-side and often in the context of web-services. In this paper, we propose a client side API-based approach to allow service substitution without any restart of the client and without any assumption on external services. Our proposition is based on a transactional approach, defined to automatically and dynamically substitute services, by preserving the current run and collected data.

Keywords: OSGi, Stale References, Substitution, Self-Healing Software

In the context of Dynamic Service-oriented Architecture(SOA), where services may dynamically appear or disappear transparently to the user, classical monitoring approaches which inject monitors into services cannot be used. We argue that, since SOA services are loosely coupled, monitors must also be loosely coupled.

In this paper, we describe an ongoing work proposing a monitoring approach dedicated to dynamic SOA systems. We defined two key properties of loosely coupled monitoring systems: dynamicity resilience and comprehensiveness. We propose a preliminary implementation targeted at the OSGi framework.

Keywords: Monitoring, Dynamic SOA, OSGi, Larva

This paper has been selected as Best Paper (Official information)

La transversalité des enseignements est de plus en plus mise en avant comme un moyen d'augmenter la qualité de la formation. Dans un contexte où les enseignements sont, par leur histoire, séparés thématiquement, l'introduction de transversalité assure une plus grande efficience de la péda- gogie et répond au besoin de s'adapter à une nouvelle génération d'étudiants. Dans cette contribution, nous présentons une démarche d'introduction de la transversalité basée sur l'externalisation des compétences. Cette démarche a été mise en oeuvre cette année à l'INSA de Lyon entre les projets d'informatique et de conception-fabrication.

Nous enseignons en 2ème année la conception, la fabrication et l'informatique autour de projets mécatroniques transverses. Nous souhaitons sensibiliser les étudiants sur le fait que leurs compétences peuvent être à la hauteur d'enjeux humanistes. L'objectif visé est de créer des liens entre leurs études et les enjeux sociétaux d'aujourd'hui leur permettant de se projeter dans le monde réel et de renforcer la motivation d'étudier. Nous décrivons ici la démarche pédagogique que nous avons adoptée.

Voici une manière simple, peut-être la plus simple, pour piloter vos circuits à distance : Android+WiFi+E-Block. Pour mémoire, Android est un système d'exploitation pour téléphones et tablettes tactiles, WiFi un ensmeble de protocoles de communication sans fil, et les E-blocks sont des modules électroniques prêts à l'emploi proposés par Elektor. Dans une série de deux articles, Android sera utilisé pour deux réalisations complètes : AndroLED et AndroCAR.

Pour piloter ce prototype, il suffit d'incliner votre téléphone Android. Celui-ci contient des accéléromètres et un module WiFi qu'il est très facile d'exploiter. Ce montage peut être réalisé très simplement et rapidement grâce à l'E-Block WiFi EB069. À partir de cet article, vous pourrez télécommander avec votre téléphone tactile et, selon vos besoins, un véhicule de la taille d'une boite d'allumettes ou faire du transport d'humains.

Software Oriented Architecture is one of the more popular and currently used architectural models. One of the essentials properties offered by this model is the loose binding between services. This property allows to indepently develop and deploy building blocks of an application. This leads to a hight mobility of the execution environment, where services can appear and disappear without a prior notivication. This paradigm brings several advantages in software designing and developpement, but there is ab big deal whis is to guaratee that applications built on top services will continue to run properly, even if the environnement is dynamic. In our work, we are interessed by one of the major problems of services communication which is services substitution. This problem is even more complex when services used are statefull. Besides, the substitution process include a look up mechanism of a compatible service, to replace the disappeared one. We work on OSGi platform and we propose an approach of services specification, in order to improve the finding of the best service for the substitution. Our contributions are then, on the first hand to provide an API based on proxies use to manage services substitutions in OSGi. On the second hand, we propose an approach of services specification based on a combined use of interface automata and CCS, to help finding the best service for the substitution.

Ce travail propose une méthode de vérification de propriétés temporelles basée sur la génération automatique d'annotations de programmes. Les annotations générées sont ensuite vérifiées par des prouveurs automatiques via un calcul de plus faible précondition. Notre contribution vise à optimiser une technique existante de génération d'annotations, afin d'améliorer l'automatisation de la vérification des obligations de preuve produites. Cette approche a été outillée sous la forme d'un plugin au sein de l'outil Frama-C pour la vérification de programmes~C.

Taux de sélection : 50%

In a model-based testing approach as well as for the verification of properties, B models provide an interesting solution. However, for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper complements previous results, based on domain abstraction for test generation, by adding a preliminary syntactic abstraction phase, based on variable elimination. We define a syntactic transformation that suppresses some variables from a B event model, in addition to a method that chooses relevant variables according to a test purpose. We propose two methods to compute an abstraction A of an initial model M. The first one computes A as a simulation of M, and the second one computes A as a bisimulation of M. The abstraction process produces a finite state system. We apply this abstraction computation to a Model Based Testing process.

Keywords: Abstraction, Test Generation, (Bi-)Simulation, Slicing.

In a model-based testing approach as well as for the verification of properties by model-checking, B models provide an interesting solution. But for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper illustrates a computer aided abstraction process that combines syntactic and semantic abstraction functions. The first function syntactically transforms a B event system M into an abstract one A, and the second one transforms a B event system into a Symbolic Labelled Transition System (SLTS). The syntactic transformation suppresses some variables in M. This function is correct in the sense that A is refined by M. A process that combines the syntactic and semantic abstractions has been experimented. It significantly reduces the time cost of semantic abstraction computation. This abstraction process allows for verifying safety properties by model-checking or for generating abstract tests. These tests are generated by a coverage criteria such as all states or all transitions of an SLTS.

In a model-based testing approach as well as for the verification of properties by model-checking, B models provide an interesting solution. But for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper illustrates a computer aided abstraction process that combines syntactic and semantic abstraction functions. The first function syntactically transforms a B event system M into an abstract one A, and the second one transforms a B event system into a Symbolic Labelled Transition System (SLTS). The syntactic transformation suppresses some variables in M. This function is correct in the sense that A is refined by M. A process that combines the syntactic and semantic abstractions has been experimented. It significantly reduces the time cost of semantic abstraction computation. This abstraction process allows for verifying safety properties by model-checking or for generating abstract tests. These tests are generated by a coverage criteria such as all states or all transitions of an SLTS.

In deductive verification of C programs increasing the automaticity of proofs is a challenging task. When applied on industrial C programs known heuristics to generate simpler verification conditions are not efficient enough. This is mainly due to their size and a high number of irrelevant hypotheses.

This work presents a strategy to reduce program verification conditions by selecting their relevant hypotheses. The relevance of a hypothesis is the combination of separated static analyses based on graph constructions and traversals. The approach is applied on a benchmark arising in industrial program verification.

Dans le cadre du développement de la plate-forme Frama-C, permettant de vérifier des programmes C annotés, nous nous sommes intéressés à la vérification par la preuve de propriétés temporelles, i.e., décrivant l'évolution du système au cours du temps.

In the verification of C programs by deductive approaches based on automated provers, some heuristics of separation analysis are proposed to handle the most difficult problems. Unfortunately, these heuristics are not sufficient when applied on industrial C programs: some valid verification conditions cannot be automatically discharged by any automated prover mainly due to their size and a high number of irrelevant hypotheses. This work presents a strategy to reduce program verification conditions by selecting their relevant hypotheses. The relevance of a hypothesis is the combination of separated static dependency analyzes based on graph constructions and traversals. The approach is applied on a benchmark issued from industrial program verification.

To document a formal model and to explain it to non specialists in formal methods , the usual approach is to use another formalism which does not require any expert skill and which gives a second viewpoint of the same model. According to this approach, we proposed in a previous paper to build a symbolic labelled transition system (SLTS) to describe behaviours of a B model. Extending this work, we now introduce hierarchies in SLTS in order to take into account the refinement process and to exhibit links between description levels. In this paper, we propose a formal definition of hierarchical-SLTS (HSLTS) and we extend the SLTS generation method in order to build a HSLTS which represents behaviours of an even-B refined model.

Cette thèse propose une approche d'aide à la conception et au développement de modèles formels B. Cette approche se base sur la construction d'un système de transitions symboliques décrivant les comportements du modèle. Cette seconde vue est complémentaire avec la description orientée données du modèle B et peut être utilisée pour le décrire, le documenter ou le valider. Le système de transitions est élaboré à partir d'un espace d'états fourni par l'utilisateur et les transitions sont construites par résolution d'obligations de preuve. Nous proposons également de prendre en compte le processus de raffinement B en introduisant la notion de hiérarchie dans les systèmes de transitions. Cette représentation permet de mettre en évidence le lien entre les données des différents niveaux de raffinement. De plus, la méthode que nous proposons se base sur la décomposition des états d'une représentation du modèle abstrait, permettant ainsi de conserver la structure générale du système. Enfin, nous terminons ce manuscrit en décrivant l'outil GénéSyst qui implante cette méthode, ainsi que son utilisation dans le cadre du projet GECCOO, pour la vérification de propriétés de sécurité.

Taux de sélection : 48%

L'objectif de cet article est de proposer une méthode de liaison des concepts abstraits d'une politique de haut niveau avec les concepts concrets d'un réseau, dans le but de pouvoir valider la conformité d'un réseau par rapport à une politique de haut niveau. Pour ce faire, nous avons suivi une approche par raffinement basée sur les différentes couches du protocole TCP/IP.

Taux de sélection : 45%

Cet article est une reprise du poster et du papier court associé présenté à Majecstic en 2005. Il correspond à une étude de cas de développement formel d'un logiciel faisant le lien entre les comportements d'un réseau et sa politique de sécurité. A cette occasion nous avons développé plus en profondeur l'expression des politiques de sécurité que nous prenons en compte et notre méthode d'implantation de notre moniteur.

Présentation de l'outil GénéSyst et des travaux l'utilisant dans le cadre de la définition et la vérification de propriétés de sécurité.

Ce document est une petite introduction au monde des cartes à puce permettant de connaître un peu mieux ce domaine. Cela permet ensuite de mieux appréhender la vérification de leurs propriétés de sécurités.

Taux de sélection : 40%

Dans cet article nous présentons une méthode permettant de vérifier des formules logiques comportementales directement sur les automates produits par l'outil GénéSyst.

Ce papier court correspond à notre premier essais de développement formel d'un logiciel faisant le lien entre les comportements d'un réseau et sa politique de sécurité. Nous y abordons les grands principes mais n'entrons pas dans le détail. Nous reprenons ce principe das un autre article basé sur un développement similaire dans la conférence AFADL 2006. A cette occasion nous avons développé plus en profondeur l'expression des politiques de sécurité que nous prenons en compte et notre méthode d'implantation de notre moniteur.

Ce poster correspond à notre premier essais de développement formel d'un logiciel faisant le lien entre les comportements d'un réseau et sa politique de sécurité. Nous y abordons les grands principes mais n'entrons pas dans le détail. Nous reprenons ce principe das un autre article basé sur un développement similaire dans la conférence AFADL 2006. A cette occasion nous avons développé plus en profondeur l'expression des politiques de sécurité que nous prenons en compte et notre méthode d'implantation de notre moniteur.

Développement de l'article de 2003 intitulé Traduction de B vers des langages de programmation qui a été sélectionné pour la revue TSI.

Taux de sélection : 46%

Présentation d'une méthode de génération, par le biais d'obligations de preuve, d'automates symboliques représentant exactement le comportement d'un système abstrait, avec prise en compte de son éventuel raffinement. L'outil GénéSyst est une implantation de ces travaux et a été présenté pour la première fois à la session outil de cette même conférence. On papier court intitulé GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel et associé à cette cession est également dans les actes.

Présentation de l'outil GénéSyst pour la session outil qui a eu lieu lors de la conférence AFADL 2004. Les fondements théoriques de cet outil sont mieux décrit dans l'article intitulé Explicitation du contrôle de développement B événementiel et présenté à cette même conférence.

Ce document est issu d'un rapport technique écrit dans le cadre du projet EDEN et servant à introduire les principaux concepts des critères communs aux différents partenaires.

Taux de sélection : 56%

Article basé sur les travaux développés dans le cadre du projet BOM (B Optimisant la Mémoire). L'objectif du projet est de produire un traducteur de B0 vers C optimisant la mémoire nécessaire au stockage d'un programme ainsi qu'à son exécution, afin de pouvoir l'embarquer sur carte à puce. Le point délicat du passage de tableaux en paramètre a notamment été abordé.