Les outils classiques de simulation ne permettent pas de prendre facilement en compte dans leur modèle, le niveau décisionnel lié à l'ordonnancement des tâches. La politique de décision est figée tout au cours d'une simulation. Par ailleurs, les outils classiques de gestion de production ne permettent pas de contrôler correctement le flux *de production, parce qu'ils ne prennent pas en compte l'état réel de l'atelier (temps mort devant les machines, pannes, ...). Ils induisent des surdimensionnements de stocke ou de mauvais taux d'utilisation des ressources. Nous proposons dans ce mémoire un outil d'aide à la conduite d'atelier flexible intégrant les aspects fonctionnement de l'atelier et gestion de production réduite au routage et à l'ordonnancement des tâches* Le simulateur proposé est basé sur l'interaction dynamique entre un interpréteur de réseaux de Petri Colorés Temporisés, garant de l'état courant de l'atelier, et un niveau décisionnel rempli par système expert. La présence d'une décision de routage, d'ordonnancement. ou la détection d'un état prédéfini se traduit au niveau de interpréteur par un conflit dans le modèle RdPCT. La construction d'un ensemble de règles de décision, par les experts humains de l'entreprise permet au système expert de résoudre le conflit. Avec l'introduction des techniques de l'Intelligence Artificielle, le système SAGASSE se caractérise par une approche ascendante du problème de conduite de l'atelier flexible, du système physique vers le système décisionnel. Des exemples industriels sont cités dans ce mémoire pour valider l'approche retenue.

Le développement et l’application des langages formels sont un défi à long terme pour la science informatique. Un enjeu particulier est l’acceptation par l’industrie. Cette thèse présente une approche pour la modélisation et la vérification des postes d’aiguillage français. La première question est la modélisation du système d’enclenchement par les réseaux de Petri colorés (RdPC). Un cadre de modélisation générique et compact est introduit, dans lequel les règles d’enclenchement sont modélisées dans une structure hiérarchique, tandis que les installations sont modélisées dans une perspective géographique. Ensuite, un patron de modèle est présenté. C’est un modèle paramétré qui intègre les règles nationales françaises qui peut être appliquée pour différentes gares. Puis, un concept basé sur l’événement est présenté dans le processus de modélisation des parties basses des postes d’aiguillage. La deuxième question est la transformation des RdPCs en machines B, qui va aider les concepteurs sur la route de l’analyse à application. Tout d’abord, une méthodologie détaillée, s’appuyant sur une table de correspondance, du RdPCs non-hiérarchiques vers les notations B est présentée. Ensuite, la hiérarchie et la priorité des transitions du RdPC sont successivement intégrées dans le processus de mapping, afin d’enrichir les possibilités de types de modèles en entrées de la transformation. Les machines B produites par la transformation permettent la preuve automatique intégrale par l’Atelier B. L’ensemble de ces travaux, chacun à leur niveau, contribuent à renforcer l’efficacité d’un cadre global d’analyse sécuritaire / Development and application of formal languages are a long-standing challenge within the computer science domain. One particular challenge is the acceptance of industry. This thesis presents some model-based methodologies for modelling and verification of the French railway interlocking systems (RIS). The first issue is the modellization of interlocking system by coloured Petri nets (CPNs). A generic and compact modelling framework is introduced, in which the interlocking rules are modelled in a hierarchical structure while the railway layout is modelled in a geographical perspective. Then, a modelling pattern is presented, which is a parameterized model respecting the French national rules. It is a reusable solution that can be applied in different stations. Then, an event-based concept is brought into the modelling process of low-level part of RIS to better describe internal interactions of relay-based logic. The second issue is the transformation of coloured Petri nets into B machines, which can help designers on the way from analysis to implementation. Firstly, a detailed mapping methodology from non-hierarchical CPNs to abstract B machine notations is presented. Then the hierarchy and the transition priority of CPNs are successively integrated into the mapping process, in order to enrich the adaptability of the transformation. This transformation is compatible with various types of colour sets and the transformed B machines can be automatically proved by Atelier B. All these works at different levels contribute towards a global safe analysis framework

Le travail présenté dans cette thèse a lieu dans le domaine de développement basé sur les composants, il est une contribution à laspécification, l'adaptation et la vérification des systèmes à base de composants. Le but principal de cette thèse est la proposition d'uneapproche formelle pour construire progressivement des systèmes complexes en assemblant et en adaptant un ensemble de composants,où leur structure et leur comportement sont modélisés à l'aide de diagrammes SysML. Dans la première étape, nous avons défini uneapproche basée sur la méta-modélisation et la transformation des modèles pour vérifier la compatibilité des blocs ayant leurs protocolesd'interaction modélisés à l'aide de diagrammes de séquence SysML. Pour vérifier leur compatibilité, nous effectuons une transformationen automates d'interface (IAs), et nous utilisons l'approche optimiste définie sur les IA. Cette approche considère que deux composantssont compatibles s'il existe un environnement approprié avec lequel ils peuvent interagir correctement. Après cela, nous avons proposéde bénéficier de la hiérarchie, qui peut être présente dans les modèles de protocole d'interaction des blocs, pour alléger la vérification dela compatibilité des blocs. Dans l'étape suivante, nous avons pris en considération le problème des incohérences de noms de type one2oneentre les services des blocs. A ce stade, un adaptateur est généré pour un ensemble de blocs réutilisés qui ont leurs protocoles d'interactionmodélisés formellement par des automates d'interface. La génération de l'adaptateur est guidée par la spécification du bloc parent qui estfaite initialement par le concepteur. Notre approche est complétée par une phase de vérification qui nous permet de vérifier les exigencesSysML, exprimées formellement par les propriétés temporelles, sur les blocs SySML. Dans cette phase, nous avons exploité uniquementles adaptateurs générés pour vérifier la préservation des exigences initialement satisfaites par les blocs réutilisés. Ainsi, notre approchea l'intention de donner plus de chance d'éviter le problème de l'explosion de l'espace d'état au moment de la vérification. Dans le mêmecontexte, où nous avons un ensemble de blocs réutilisés et la spécification de leurs blocs parents, nous avons proposé d'utiliser des réseauxde Petri colorés (CPN) pour modéliser les interactions des blocs et générer des adaptateurs qui résolvent plus de types de problèmes. Dansce cas, l'adaptateur peut résoudre le problème de blocage en permettant le ré-ordonnancement des appels de services. / The work presented in this thesis takes place in the component-based development domain, it is a contribution to the specification,adaptation and verification of component-based systems. The main purpose of this thesis is the proposition of a formal approach tobuild incrementally complex systems by assembling and adapting a set of components, where their structure and behaviour are modelledusing SysML diagrams. In the first stage, we have defined a meta-model driven approach which is based on meta-modelling and modelstransformation, to verify the compatibility of blocks having their interaction protocols modelled using SysML sequence diagrams. To verifytheir compatibility, we perform a transformation into interface automata (IAs), and we base on the optimistic approach defined on IAs. Thisapproach consider that two components are compatible if there is a suitable environment with which they can interact correctly. Afterthat, we have proposed to benefit from the hierarchy, that may be present in the interaction protocol models of the blocks, to alleviate theverification of blocks compatibility. In the next stage, we have taken into consideration the problem of names mismatches of type one2onebetween services of blocks. At this stage, an adapter is generated for a set of reused blocks which have their interaction protocols modelledformally by interface automata. The generation of the adapter is guided by the specification of the parent block which is made initiallyby the designer. Our approach is completed by a verification phase which allows us to verify SysML requirements, expressed formallyby temporal properties, on SySML blocks. In this phase, we have exploited only the generated adapters to verify the preservation of therequirements initially satisfied by the reused blocks. Thus, our approach intends to give more chance to avoid the state space explosionproblem during the verification. In the same context, where we have a set of reused blocks and the specification of their parent blocks, wehave proposed to use coloured Petri nets (CPNs) to model the blocks interactions and to generate adapters that solve more type of problems.In this case the adapter can solve the problem of livelock by enabling the reordering of services calls.