Spécification, modélisation et vérification d'une architecture multi-agents dédiée à la gestion des risques de collision automobile
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
Computer sciences take a rising place in various industrial systems, complex spatial equipment are for instance controlled by computer systems. The equipment operates correctly when the behavior of the computer part is correct. Thus, verification methods are of great importance, as they prove the correct behavior according to rigorous and exhaustive analyses based on strong theories, the methods also bring appropriated tools. Within the verification scheme, a model of the system is described using languages which semantics associate to the model a state graph that represents all possible executions. This space makes it possible the identification of such states or sequences which are not allowed. The construction of this graph may lead to the combinatorial explosion problem. This key step takes thus preponderant place in this thesis, here are considered various construction strategies with reduction, based on partial orders and equivalency relations : verification tools implementing these strategies are compared according to various classical case studies. A more complex case study, that concerns an agent based system dedicated to road collision risks management, has also been dealt with. Consequently, specification, graph construction and verification aspects were considered. This part of the study associates researchers from different areas, highlighting key points of complex systems design. This collaboration allowed the definition of abstractions, focusing on interactions, reducing thus the size of state graphs, making possible the verification step. Modeling, within tools languages, of parallel processing, led us to propose several control schemes which verifications all succeeded.
Abstract FR:
L'informatique prend une place importante dans les systèmes de divers secteurs d'activités, des dispositifs sophistiqués de l'industrie spatiale sont ainsi pilotés par des systèmes informatiques. Le bon fonctionnement repose alors sur le comportement correct de ces derniers. Aussi, la place des méthodes de vérification est importante, car apportant une garantie de bon fonctionnement rigoureuse et exhaustive, basée sur une approche théorique solide et des outils de génie logiciel réalisant les fondements théoriques. Dans le schéma de la vérification, un modèle du système est décrit dans un langage où la sémantique opérationnelle associe au modèle un graphe d'états, décrivant toutes les exécutions possibles, dans lequel peuvent être identifiés des séquences ou des états prohibés. La construction de ce graphe peut conduire à l'explosion combinatoire. Cette étape clé prend donc une place prépondérante dans les travaux de cette thèse où sont considérées différentes stratégies, de construction avec réduction, basées sur des ordres partiels et des relations d'équivalences : des outils de vérification les implantant ont été confrontés, par rapport à différentes études de cas classiques. Une étude de cas conséquente a été aussi menée sur un système basé agents d'aide à la conduite automobile, amenant à aborder des aspects spécification, construction de graphe et vérification. Cette étape a associée des spécialistes de communautés différentes, mettant en relief divers éléments d'un processus de conception de systèmes complexes. Cette collaboration a permis de définir les abstractions, en se focalisant sur le contrôle des interactions des agents, permettant ainsi la réduction de la taille du graphe d'états, rendant alors possible la vérification. La modélisation, dans les langages des outils visés du parallélisme des traitements, nous a aussi conduit à proposer plusieurs versions de schémas de contrôles et leurs vérifications ont toutes réussies.