Search

Internet of Things applications impact more and more industrial areas such as smart manufacturing, smart health monitoring and home automation; physical objects or devices equipped with sensors and actuators are interconnected and then controlled with software applications. Ensuring the correct construction, the well-functioning and the reliability of these applications constitute important issues for some of these applications which can be critical in case of dysfunction. We propose on the basis of the formal model of their common architectural properties, a generic framework for the formal modelling of IoT-based applications, the rigorous analysis of their consistency properties, their rigorous construction and evolution. Specific properties can be gradually added and checked. The proposed framework is then implemented and experimented using Event-B. We exploit the observation that the main requirements of the IoT-based physical architectures and control software are common to all IoT-based applications; this leaded us to the definition of the generic formal model together with invariant architectural and consistency properties. The proposed approach is generic, extensible, and can be profitably adapted to more general hybrid or cyber-physical systems. Our current implementation is independent of the formal model, it can be achieved in various other formal analysis environments., (16 pages, work in progress)

International audience

Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot's Lambda Mu Calculus and Curien-Herbelin's Lambda Bar Mu Mu Tidle Calculus. We aim at showing their computational equivalence. We define translations between these calculi. We prove simulation theorems for an undirected evaluation as well as for call-by-name and call-by-value evaluations.

L'objectif de ce travail de thèse consiste à fournir une démarche formelle pour la vérification de circuits numériques conçus en sécurité, c'est-à-dire qui sont prévus pour gérer certaines de leurs défaillances. Par démarche formelle, nous entendons le fait de pouvoir associer une signification mathématique et précise aux comportements des circuits numériques tant en mode normal, en l'absence de défaillance, qu'en mode dégradé, en présence de défaillances. Le but de ce travail est de permettre de déterminer dans quel contexte de défaillances un circuit numérique est sûr de fonctionnement. Le travail réalisé consiste, dans un premier temps, à enrichir un langage de spécification et de description des circuits numériques afin d'exprimer que des fautes -c'est-à-dire les causes de leurs défaillances - s'appliquent dessus et comment elles modifient le comportement des circuits numériques. Le premier objectif de cette thèse correspond donc à la formalisation des fautes de circuits numériques. Le second objectif correspond à l'élaboration d'un processus de vérification des circuits numériques en présence de fautes. Plus précisément, il s'agit de vérifier si leurs comportements sont sûrs de fonctionnement. Cet objectif est atteint en étendant les techniques de vérification existantes pour les circuits numériques. Thèse encadré par Mariano,G (INRETS) et Boulanger,JL (UTC)