Le but de ce travail est de proposer un système formel pour prouver que l'ensemble des succès d'un programme logique est inclus dans l'ensemble correspondant d'un autre programme. Cela permet de prouver que deux programmes logiques, un qui représente la spécification et un représentant l'implantation sont équivalents. Le langage logique considéré est CLPforall qui est le langage le langage de programmation logique avec contraintes (CLP) auquel est ajouté le quantificateur universel. Nous présentons les sémantiques des succès finis et infinis et montrons qu'elles sont données par le plus petit et le plus grand point fixe du même opérateur. Un système de preuve pour l'inclusion des succès finis est présenté. Le système utilise pour les opérateurs et les quantificateurs logiques les mêmes règles que la logique du premier ordre. Pour raisonner sur les prédicats récursifs le système contient une règle d'induction. Nous prouvons la correction du système sous certains conditions. Un système analogue pour l'inclusion des succès infinis est présenté. La règle d'induction est remplacée par une règle de coinduction. La correction est démontrée sous conditions analogues. Les deux systèmes sont équivalents sous certains conditions. Une implantation a été réalisée sous la forme d'assistant de preuve écrit en Prolog. Le programme a environ 4000 lignes et contient des procédures simples mais efficaces de recherche de preuves. Nous présentons des exemples de preuves réalises avec ce programme parmi lesquels la preuve de correction de quicksort.

L'éducation populaire est un apprentissage collectif à la compétence diagnostique, à l'argumentation rationnelle, à la réflexion critique sur la participation citoyenne pour que chacun puisse conscientiser son expérience sociale. Les animateurs socioculturels sont des généralistes de la relation pour dialoguer et de l'association pour agir ensemble avec une visée de renforcement ou de transformation du lien social. La relation des bénévoles et des professionnels est un assemblage délicat pour démultiplier la compétence collective de s'associer qui nécessite de partager des valeurs sur le projet politique. Le système de l'éducation nonformelle doit faire reconnaître sa visée éducative dans les socialisations intergénérationnelles, dans l'éducation permanente tout au long de la vie, dans la démocratie culturelle, dans la citoyenneté participative. L'association représente un espace d'autoformation sur un territoire de proximité : une situation d'écoute et de coopération, un débat sur les besoins des populations, une analyse critique de l'action sociale et politique, la construction de réponses alternatives. L'éducation du citoyen est une éducation à la discussion pour comprendre les problèmes et débattre des politiques envisagées pour y répondre. La posture de résolution de problèmes s'acquiert en évaluant, en expérimentant, en prenant des risques ensemble, et en délibérant pour choisir. La communauté réflexive et dialogique construit un savoir sur les contextes et une interprétation de la réalité pour produire du sens et dépasser les préjugés, l'évaluation de la situation permet de penser des actions pour essayer de modifier l'environnement et les interactions inégalitaires

La mise en oeuvre des méthodes formelles déductives lors du développement de systèmes permet d'obtenir des garanties mathématiques quant à leur validité. Pour cette raison, leur utilisation est recommandée ou exigée par certains standards relatifs à la sûreté de fonctionnement ou à la sécurité, tels que l'IEC 61508 ou les Critères Communs. Il reste cependant légitime de s'interroger sur la portée exacte des bénéfices obtenus. Certains aspects d'un système peuvent en effet échapper à la formalisation, et il n'est pas toujours facile d'identifier ces limitations ou leurs conséquences. De même, si la validité d'une preuve vérifiée mécaniquement est difficilement contestable, son utilisation pour justifier d'une confiance réelle dans le système physique n'est pas toujours admise. De telles questions sont particulièrement pertinentes dans le domaine de la sécurité, lorsque les systèmes sont l'objet d'attaques de la part d'agents intelligents ; par rapport à la sûreté il y a un changement radical de point de vue, qui justifie de s'interroger quant à l'application de principes ou de pratiques bien connus. Nous identifions les bénéfice et évaluons la confiance résultant de l'application des méthodes formelles déductives lors de développements de systèmes de sécurité. Cette analyse aborde les éventuelles difficultés, déviations ou problèmes qui peuvent être rencontrés et les illustre par des exemples. Elle comporte également une étude détaillée du concept de raffinement, et présente un plongement profond visant à valider la logique de la méthode B en Coq. Ce plongement conduit par ailleurs à l'étude des représentations à la de Bruijn.

L'étude des grands modèles de réseaux biologiques par l'utilisation d'outils d'analyse et de simulation conduit à un grand nombre de prédictions. Cela soulève la question de savoir comment identifier les prédictions intéressantes de nouveaux phénomènes, qui peuvent être confrontés à des données expérimentales. Les techniques de vérification formelle basées sur le model checking constituent une technologie puissante pour faire face à cette augmentation d'échelle et de complexité pour l'analyse de ces réseaux. L'application de ces techniques est par contre difficile, pour plusieurs raisons. Premièrement, le domaine de la biologie des systèmes a mis en évidence quelques propriétés dynamiques du réseau, comme la multi-stabilité et les oscillations, qui ne sont pas facilement exprimables avec les logiques temporelles classiques. Deuxièmement, la difficulté de poser des questions pertinentes et intéressantes en logique temporelle est difficile pour les utilisateurs non-experts. Enfin, la plupart des modèles existants et des outils de simulation ne sont pas capables d'appliquer des techniques de model checking d'une manière transparente. La mise en œuvre des approches développées dans ce travail contribue à enlever des obstacles pour l'utilisation de la technologie de vérification formelle en biologie. Leur application a été validée sur l'analyse et la simulation de deux modèles biologiques complexes.

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette thèse sous l'angle de la mise en œuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions, la solution actuellement privilégiée dans l'industrie. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système

La réglementation de la sécurité est un des déterminants principaux de la sécurité du transport maritime. Depuis la fin du 20ème siècle, de nouvelles approches normatives fondées sur les risques viennent compléter la configuration traditionnelle - déterministe et prescriptive - de la réglementation de la sécurité. Nos travaux de recherche traitent de l'intérêt des techniques d'évaluation du risque pour la réglementation de la sécurité. Le travail méthodologique de production et d'organisation des concepts théoriques et des apports de terrain relatifs aux configurations réglementaires " non traditionnelles " permet de formaliser l'utilisation des techniques d'évaluation du risque et de proposer des aspects influençant le choix des techniques. Deux méthodes d'évaluation du risque sont améliorées - relatives à (i) l'évaluation formelle de la sécurité à utiliser dans le cadre du processus d'élaboration de règles, et aux (ii) conceptions alternatives pour la sécurité incendie à utiliser dans le cadre de conceptions de navire ne répondant pas aux exigences réglementaires classiques - et mises en oeuvre, respectivement, pour la sécurité des vraquiers et pour un espace public de navires à passagers. A travers ce travail, nous avons pu mettre en évidence l'utilisation potentielle de l'évaluation du risque pour la réglementation de la sécurité, et dégager les grandes lignes structurant ces approches.

Dans les années 90, la commission européenne a sollicité la mise au point d'un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS " European Railway Traffic Management System ". Il s'agit d'un système réparti complexe dont le déploiement complet est long et coûteux. L'objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d'une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d'autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L'objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS

Cette Habilitation à Diriger des Recherches est le fruit des résultats, tant en recherche qu'en enseignement ou en transfert, de mon activité d'enseignant chercheur. Initiée au sein du Laboratoire d'Informatique, de Microélectronique et de Robotique de Montpellier (LIRMM, UMR CNRS/UM2) de 1991 à 1994, cette activité s'est ensuite concrétisée au sein du Laboratoire de Génie Informatique et d'Ingénierie de Production (LGI2P) de l'Ecole des Mines d'Alès où j'exerce depuis 1994.<br />Le travail de recherche entrepris depuis le début du Doctorat en 1991 relève de la thématique de la modélisation de systèmes complexes puis de la vérification et de la validation de ces modèles. Ceci a pour objectif d'assurer, ou à défaut de rassurer, le modeleur sur la qualité des modèles, sur leur pertinence vis-à-vis du système considéré et sur le respect d'exigences qui ont présidé à leur construction. La recherche a donc consisté au développement d'approches de modélisation, de spécification formelle de propriétés, de vérification par preuve de propriétés au moyen de Graphes Conceptuels et de simulation comportementale. Les domaines d'application privilégiés ont été les systèmes de contrôle commande répartis, puis plus largement la modélisation d'entreprise et tentent aujourd'hui d'intégrer une dimension risque dans la modélisation d'entreprise et de s'ouvrir plus largement à l'ingénierie des systèmes complexes. Les résultats sont des langages et un cadre de modélisation intégré, un langage de spécification baptisé LUSP, une suite de mécanismes de preuve formelle et de simulation qui ont donné lieu à divers encadrements de thèses, de travaux et à des transferts vers l'industrie. <br />Enfin, l'activité d'enseignement a tenté de rester cohérente avec le profil de compétence à la fois de producticien et d'ingénierie système acquis ou inspiré par la thématique de recherche. Elle s'est déroulée dans le cadre de diverses Universités, Ecoles d'Ingénieurs ou de cursus spécialisés. Les résultats sont des propositions et l'accompagnement de thématiques nouvelles, une activité d'ingénierie pédagogique et une implication dans diverses responsabilités administratives.

De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Cette thèse porte sur la vérification formelle de systèmes temps réel et procède par transformation de modèle entre l'algèbre de processus temporisée RT-LOTOS et les réseaux de Petri temporels étendus par des chronomètres et des données. Des schémas de traduction de RT-LOTOS vers ces réseaux de Petri étendus sont proposés et formellement prouvés. L'approche transformationnelle développée pour la partie " contrôle " de RT-LOTOS est étendue à la partie " données ". Le langage RT-LOTOS est lui même enrichi d'un opérateur de suspension reprise qui permet de modéliser et vérifier une classe plus large de systèmes temps réel Plusieurs études de cas attestent de l'efficacité des schémas de traduction proposés par rapport à des outils LOTOS ou RT-LOTOS développés antérieurement. L'approche proposée s'avère transposable à d'autres langages de modélisation en particulier le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment).