Construction d'un platoon en CSPllB

• المؤلفون الرئيسيون: JACQUOT, Jean-Pierre, SOUQUIERES, Jeanine, NGUYEN, Huu Nghia
• التنسيق: Theses and Dissertations
• اللغة: French
• منشور في: 2015
• الموضوعات: CSPIIB; composants logiciel; platoon; vérification formelle
• الوصول للمادة أونلاين: http://repository.vnu.edu.vn/handle/VNU_123/338
• المؤسسة: Vietnam National University, Hanoi

Ce travail a été réalisé dans le cadre des projets TACOS et CRISTAL qui ont pour but de construire un système des véhicules autonomes en libre-service. Dans ce système, les véhicules peuvent se déplacer en convoi. Nous partons d'une modélisation d'un convoi en CSPjjB. Elle décrit les processus internes des véhicules membres qui maintiennent la distance entre véhicules, de sorte que la propriété de déplacement en convoi est conservée. Le travail de stage a eu pour premier but de modéliser en CSPjjB les processus internes des véhicules pour accrocher et décrocher d'un convoi. Nous avons amélioré le modèle existant pour avoir un nouveau modèle qui présente les processus de quatre modes de fonctionnement : déplacement en convoi, décrochage d'un convoi, déplacement indépendant et accrochage à un convoi. Un second axe a été consacré à la théorie de l'approche CSPjjB. CSPjjB, qui apparait dans les années 2000, est la combinaison de la méthode B et de l'algèbre CSP. Elle n'est pas encore totalement achevée. Une modélisation en CSPjjB comporte plusieurs composants CSPjjB. Chaque composant CSPjjB contient une machine B et un contrôleur CSP. Il existe des outils pour vérifier les machines B et leur contrôleur CSP. Cependant, il n'existe pas encore d'outil qui permet de vérifier la cohérence entre la machine B et son contrôleur CSP. Nous avons construit un logiciel qui permet de résoudre ce problème.