Institut National des Sciences Appliquéees de Lyon CITI Laboratory Université de Lyon

Publications

2017

Article court :
  • Oscar CARRILLO, Nicolas STOULS, Raphael LAURENT, Nikolai PLOKHOI, Qifan ZHOU, Julien PONGE et Frédéric LE MOUËL HardenedGolo : pour augmenter le niveau de confiance en un code Golo 16èmes journées sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'17) ( HAL, .bib, .pdf)

    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.

Publication pédagogique avec comité national :
  • François Lesueur et Nicolas Stouls Le Libre : catalyseur de l'Humanisme ? 5è colloque Pédagogie et Formation Inter INSA, Mars 2017, Lyon, France. ( HAL, .bib, .pdf)

    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

  • Nicolas Stouls, Oscar Carrillo, Julien Ponge, Frédéric Le Mouël et Alexandre Claude Apprentissage augmenté : le numérique comme outil d'aide à l'apprentissage 5è colloque Pédagogie et Formation Inter INSA, Mars 2017, Lyon, France. ( HAL, .bib, .pdf)

    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

2016

Conférence avec comité de programme international :
  • Roya Golchay, Frédéric Le Mouël, Julien Ponge and Nicolas Stouls Spontaneous Proximity Clouds: Making Mobile Devices to Collaborate for Resource and Data Sharing Proceedings of the 12th EAI International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom'2016), Nov 2016, Beijing, China ( Conférence, HAL, .bib, .pdf)

    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.

  • Roya Golchay, Frédéric Le Mouël, Julien Ponge and Nicolas Stouls, Automated Application Offloading through Ant-inspired Decision-Making Proceedings of the 13th International Conference on New Technologies in Distributed Systems (NOTERE'2016), Jul 2016 ( HAL, .bib, .pdf)

    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

2015

Conférence avec comité de programme international :
  • Baptiste Maingret, Frédéric Le Mouël, Julien Ponge, Nicolas Stouls, Jian Cao and Yannick Loiseau, Towards a Decoupled Context-Oriented Programming Language for the Internet of Things ACM, 7th International Workshop on Context-Oriented Programming (COP'2015) in conjunction with the European Conference on Object-Oriented Programming (ECOOP'2015), pp.6-11, 2015 ( HAL, ACM, .bib)

    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.

Rapport de recherche :
  • Julien Ponge, Frédéric Le Mouël, Nicolas Stouls, Yannick Loiseau Opportunities for a Truffle-based Golo Interpreter . ( .bib, HAL)

    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.

Publication pédagogique avec comité national :
  • Guy ATHANAZE, Virginie BARAUD, Jean-Marie BLUET, Marielle de PASQUA, Brice GAUTIER, Carine GOUTALAND, Rémy HERVE, Richard MOREAU, Pierre MICHAUD, Alexandra PETIT, Philippe STEYER, Nicolas STOULS, Erin TREMOUILHAC, Évaluation de l'enseignement au premier cycle de l'INSA Lyon -- Un chantier de taille, qui demeure ouvert. Dans les actes du 4ème colloque international pédagogie et formation, les 2 et 3 Avril 2015. ( .pdf)

    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.

2014

Conférence avec comité de programme international :
  • Akram Idani and Nicolas Stouls, When a Formal Model Rhymes with a Graphical Notation. The First Human-Oriented Formal Methods workshop, LNCS Volume 8938, pp 54-68, 2015 ( HAL, Springer, .bib)

    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.

  • Yufang Dan, Nicolas Stouls et Stephane Frenot An OSGi Monitoring System with Dynamicity Resilience enhancing Fault Tolerance. The Fifth International Conferences on Software and Computing Technology, ICSCT 2014, Lijiang, China. ( HAL, .bib)

    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.

2013

Revue avec comité de programme international :
  • Yufang Dan, Nicolas Stouls, Christian Colombo and Stéphane Frénot OSGiLarva: a Monitoring Framework Supporting OSGi's Dynamicity. In International journal on advances in security Vol. 6, 1&2 (2013), pp. 49-61, ISSN 1942-2636. Revised and extended version of a SERVICE COMPUTATION 2012 paper. ( .bib, HAL, Think Mind)

    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.

  • J. Julliand, N. Stouls, P-C. Bué et P-A. Masson B Model Slicing and Predicate Abstraction to Generate Tests. In SQJ, Software Quality Journal, Springer, March 2013, Volume 21, Issue 1, pp 127-158. Revised and extended version of a TAP'10 paper. ( .bib, .pdf, .ps.gz, LNCS)

    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.

Article court :
  • Julien Ponge, Frédéric Le Mouël and Nicolas Stouls Golo, a Dynamic, Light and Efficient Language for Post-Invokedynamic JVM PPPJ - International Conference on Principles and Practices of Programming on the Java platform: virtual machines, lamguages and tools - 2013 ( .pdf, HAL, ACM)

    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

Poster :
  • Roya Golchay, Frédéric Le Mouël, Julien Ponge et Nicolas Stouls Les smartphones comme passerelle de services : peuvent-ils relier l'Internet des choses (IoT) et la virtualisation dans les nuages (Cloud) ? Conférence d'informatique en Parallélisme, Architecture et Système (ComPAS) - Conférence Française en Systèmes d'Exploitation (CFSE 2013) ( .pdf, HAL)

    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

2012

Conférence avec comité de programme international :
  • Herman Mekontso Tchinda, Julien Ponge, Yufang Dan et Nicolas Stouls An API for Autonomous and Client-side Service Substitution. The Fourth International Conferences on Advanced Service Computing, SERVICE COMPUTATION 2012, pages 14--19, ISBN 978-1-61208-215-8 ( .bib, .Think Mind, .pdf)

    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

Article court :
  • Yufang Dan, Nicolas Stouls, Stéphane Frénot and Christian Colombo, A Monitoring Approach for Dynamic Service-Oriented Architecture Systems. The Fourth International Conferences on Advanced Service Computing, SERVICE COMPUTATION 2012, pages 20--23. ISBN 978-1-61208-215-8. ( .bib, .Think Mind, .pdf)

    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)

Publication pédagogique avec comité national :
  • Emmanuel Cartillier, Nicolas Stouls, Benoit Pierret et Yann Ricotti, Externalisation de la transversalité : vers une pérennité des enseignements transverses -- Exemple d'un projet réalisé en partenariat via le projet CRITER. Dans les actes du colloque Formation, pédagogie : Partage d'expériences et innovations, les 17 et 18 avril 2012. ( .pdf)

    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.

  • RICOTTI Yann, EGLIN Véronique, PIERRET Benoit, STOULS Nicolas et MOREAU Richard, Un projet humain au service de la société comme support d'enseignement de la mécatronique, l'informatique et la productique -- Un Simulateur de conduite pour le service rééducation de l'hôpital Marrel de Rive de Gier. Dans les actes du colloque Formation, pédagogie : Partage d'expériences et innovations, les 17 et 18 avril 2012. ( .pdf)

    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.

Publication grand publique :
  • Nicolas Stouls, Benoit Pierret et Yann Ricotti, AndroLED -- votre électronique pilotée via le WiFi sous Android. Elektor, n°411, pages 48--53, Septembre 2012. ( .bib, HAL)

    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.

  • Benoit Pierret, Nicolas Stouls et Yann Ricotti, AndroCAR. Elektor, Octobre 2012. ( .bib, HAL)

    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.

2011

Rapport de recherche :
  • Albert Herman Mekontso Tchinda, Nicolas Stouls et Julien Ponge, Spécification et substitution de services OSGi ( .bib, HAL)

    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.

  • N. Stouls et J. Groslambert Vérification de propriétés LTL sur des programmes C par génération d'annotations. ( .bib, HAL)

    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.

2010

Conférence avec comité de programme international :
  • J. Julliand, N. Stouls, P-C. Bué et P-A. Masson Syntactic Abstraction of B Models to Generate Tests.. In G. Fraser and A. Gargantini, editors, TAP'10, 4th Int. Conf. on Tests and Proofs, volume 6143 of LNCS, Malaga, Spain, pages 151--166, July 2010. ( .bib, .ps.gz, .pdf, LNCS)

    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.

Article court :
  • J. Julliand, N. Stouls, P-C. Bué et P-A. Masson B Model Abstraction Combining Syntactic and Semantic Methods. ABZ 2010, LNCS, page 408. ( .bib, .pdf, LNCS)

    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.

Rapport de recherche :
  • J. Julliand, N. Stouls, P-C. Bué et P-A. Masson B Model Abstraction Combining Syntactic and Semantics Methods. LIFC Research Report RR2009-04. ( .bib, .pdf)

    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.

2009

Conférence avec comité de programme international :
  • J.-F. Couchot, A. Giorgetti and N. Stouls. Graph-based Reduction of Program Verification Conditions. . In proceedings of AFM'09, colocated with CAV'09, pages 40-47. ( .bib, .ps.gz, .pdf)

    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.

Article court :
  • J. Groslambert et N. Stouls. Vérification de propriétés LTL sur des programmes C par génération d'annotations. AFADL 2009 ( .bib, article.ps.gz, article.pdf, exposé.ps.gz, exposé.pdf)

    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.

Exposés :
  • Présentation d'introduction aux méthodes formelles aux membres du CITI ( .pdf, .ps.gs)

2008

Rapport de recherche :
  • Jean-François Couchot and Alain Giorgetti and Nicolas Stouls. Graph-based Reduction of Program Verification Conditions INRIA Saclay -- Île-de-France, RR-6702, 22 pages ( HAL)

    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.

  • N. Stouls. Computation of Hierarchical Transition Systems to Document Refined Event-B Models. ( .bib, HAL)

    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.

Exposés :
  • Présentation de l'outil Aoraï au groupe de travail 1.4 du projet PFC ainsi qu'en séminaire à l'équipe ProVal de l'INRIA Saclay ( .pdf, .ps.gs)
  • Séminaire CITI présentant la séléction d'hypothèses ( .pdf, .ps.gs)

2007

Thèse de doctorat :
  • N. Stouls. Systèmes de transitions symboliques et hiérarchiques pour la conception et la validation de modèles B raffinés (.bib, .ps.gz, .pdf), Institut Polytechnique de Grenoble. (Transparents de la soutenance : .ps.gz, .pdf)
    Composition du jury :
    Jean-Claude FernandezPrésident Professeur à l'université de Grenoble 1
    Marie-Laure Potet Directeur de thèseProfesseur à l'IP Grenoble
    Sylvain Boulmé Co-encadrant Maître de conférence à l'IP Grenoble
    Jacques Julliand Rapporteur Professeur à l'université de Franche Comté
    Michael Leuschel Rapporteur Professeur à l'université de Düsseldorf
    Claude Marché Examinateur Directeur de recherche à l'INRIA-Futurs
    Christophe Planat Examinateur ST-Microelectronics

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

Conférence avec comité de programme international :
  • N. Stouls. and M-L Potet. Security policy enforcement through refinement process. LNCS n°4355 p.216-231, Springer-Verlag, In proceedings of B'07. ( .bib, .ps.gz, .pdf, LNCS)

    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.

Exposés :
  • Présentation des premières expérimentations d'OSLO ( .pdf, .ps.gs)
  • Séminaire de présentation de mes travaux de thèse à l'équipe TFC du LIFC, Besançon.
Divers :
  • Participation à la fête de la science 2007 dans l'atelier organisé à l'université d'Orsay par Florence Plateau et Yannick Moy.

2006

Conférence avec comité de programme national :
  • Nicolas Stouls et Vianney Darmaillacq. Développement formel d'un moniteur détectant les violations de politiques de sécurité de réseaux, AFADL 2006. ( .bib, .ps.gz, .pdf)

    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.

Poster :
  • N. Stouls. Aide à la spécification et au développement formel de systèmes. 16ème rencontres régionales de la recherche en rhône-alpes 2006 ( .bib, .pdf, .ps.gz)

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

Rapport de recherche :
  • N. Stouls. Introduction aux cartes à puce. ( .bib, .pdf, .ps.gz, .html, HAL)

    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.

Exposés :
  • Séminaire invité à Abo University, Turku, Finlande.

2005

Conférence avec comité de programme international :
  • D. Bert, M-L. Potet et N.Stouls. GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties. LNCS n°3455 p.299-318, Springer-Verlag, ZB 2005. ( .bib, .ps.gz, .pdf, LNCS)

    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.

Poster :
  • Nicolas Stouls et Vianney Darmaillacq. Développement formel d'un moniteur. Majecstic 2005. ( .bib, .pdf, .ps.gz)

    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.

  • Nicolas Stouls et Vianney Darmaillacq. Développement formel d'un moniteur. Majecstic 2005. ( .bib, .pdf)

    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.

Exposés :
  • Présentation aux membre du projet RNTL PoTestAT : Modélisation et raffinement d'une politique de contrôle d'accès en B ( .pdf)
  • Bilan des travaux effectués sur DEMONEY dans le cadre de GECCOO ( .pdf, .ps.gs)

2004

Revue avec comité de programme international :
  • Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls et Laurent Voisin. Adaptabilité et validation de la traduction de B vers C - Points de vue du projet BOM. Technique et Science Informatiques, RSTI, série TSI, numéro 7/2004, Hermès-Lavoisier. ( .pdf, .bib, TSI E-Revues)

    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.

Conférence avec comité de programme national :
  • N. Stouls et M-L. Potet. Explicitation du contrôle de développement B événementiel, AFADL 2004 ( .bib, .ps.gz, .pdf)

    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.

Article court :
  • X. Morselli, M.-L. Potet et N. Stouls. GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel. AFADL 2004, Session outils ( .bib, .pdf, .ps.gz)

    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.

Rapport de recherche :
  • N. Stouls. Documentation d'introduction aux critères communs. ( .bib, .pdf, .ps.gz, .html, HAL)

    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.

Exposés :
  • Séminaire aux thésards du LSR : Vérification de propriétés de sécurité sur des modèles B ( .pdf, .ps.gs)
  • Présentation au groupe de travail AFADL : Vérification de propriétés de sécurité sur des modèles B ( .pdf, .ps.gs)
  • Présentation au groupe de travail du projet RNTL GECCOO : Vérification de Propriétés de sécurité ( .pdf)
  • Séminaire LSR de présentation des langages VHD, SystemC et Verilog : Verilog / VHDL / SystemC What is that ?
  • Présentation au groupe de travail du projet RNTL GECCOO : DEMONEY : Modélisation en B et vérification de propriétés ( .pdf)
  • Présentation au groupe de travail du projet RNTL GECCOO : DEMONEY : description et cas d'application au projet GECCOO ( .pdf)

2003

Conférence avec comité de programme national :
  • F. Badeau, D. Bert, S. Boulmé, C. Métayer, M-L. Potet, N. Stouls et L. Voisin. Traduction de B vers des langages de programmation. AFADL 2003. ( .bib)

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

Retour au plan

SHT75DHT22LM35
Température : °C  [°C .. °C]°C  [°C .. °C]°C
Humidité : %  [% .. %]%  [% .. %] 
Point de rosée : °C  [°C .. °C]  
Indice de chaleur :  °C  [°C .. °C] 

Up-time : 0j, 0h et 0m.

Ces données vous ont été généreusement offertes par Arduino (Yun), wikipedia, la DSI, le CISR et la direction du patrimoine.