Etude et Conception de Systèmes avec Perturbations – ECSPER

La correction des logiciels demeure un enjeu important, en particulier dans le cadre des systèmes distribués et embarqués. Au cours des dernières décennies, de nombreux travaux ont concerné l'utilisation de méthodes formelles pour la preuve de la correction de systèmes, et notamment des méthodes automatiques comme le model checking. Ces méthodes permettent de traiter le non déterminisme des modèles, et de fournir une analyse exhaustive du système. Ceci contraste avec les méthodes de simulation et de test qui ne peuvent pas capturer l'ensemble des comportements. Le non déterminisme est utilisé en modélisation pour différents objectifs : 1. la modélisation de systèmes ouverts dans lesquels un environnement décide de ses propres opérations. Dans ce cas, les actions de l'environnement sont modélisées de façon non déterministe afin de représenter le comportement d'un système dans un environnement quelconque. 2. le non-déterminisme introduit par abstraction afin de permettre l'analyse du système. Un exemple typique est la discrétisation de variables continues dans des intervalles de valeurs. 3. le non-déterminsime comme un modèle pour les comportements perturbés. Bien que formellement ceci puisse être vu comme un sous-cas de 2, cela constitue un sujet à part entière dans la mesure où il est spécialisé à la représentation des déviations par rapport au comportement nominal. Un exemple de tel non déterminisme est la modélisation de canaux à pertes, qui diffèrent des canaux FIFO idéaux dans la mesure où ils peuvent perdre des messages. Un autre exemple est l'introduction de dérives d'horloges dans les automates temporisés. Ce projet s'intéresse au troisième type de non déterminisme, que nous appelons perturbations. Ceci contraste avec les techniques utilisant des méthodes probabilistes, comme c'est le cas dans le domaine de la tolérance aux fautes. Définir les perturbations à l'aide d'une sémantique alternative fondée sur le non déterminisme permet d'utilise des techniques dédiées aux systèmes non déterministes (comme les approches symboliques) ce qui permet une analyse exhaustive. Un enjeu principal de la vérification automatique est l'existence de procédures de décision et d'algorithmes efficaces pour les problèmes examinés. Tandis que le model checking a été à l'origine introduit pour les systèmes à états finis, il existe aujourd'hui de nombreuses extensions pour des systèmes infinis (temps dense, compteurs non bornés, files...) Dans cette direction, les perturbations peuvent, de façon surprenante, permettre de simplifier l'analyse des systèmes. Par exemple, tandis que le problème de sûreté pour les automates hybrides indécidable, il a été démontré que pour les systèmes robustes, i.e. tolérants aux perturbations, le problème devient décidable. Des observations similaires ont été faites pour d'autres types de modèles et dans différents contextes mais, à notre connaissance, peu d'effort a été investi pour un examen croisé de ces différents types de perturbations et des algorithmes associés. D'un autre côté, la plupart des travaux sur les perturbations s'intéressent essentiellement à des aspects théoriques/techniques mais pas à l'utilisation de ces modèles pour des applications réelles. Par exemple la perte de message des "lossy channel systems" semble d'un usage limité pour les applications, puisque les communications peuvent être stoppées. Buts du projet : Le projet vise à progresser dans la compréhension des perturbation vis-à-vis de la vérification automatique et de la modélisation. Nous voulons comprendre si et comment les différents types de perturbations et les algorithmes associés sont liés, étudier ces interacions et proposer de nouveaux modèles de perturbations possédant les propriétés attendues. Nous souhaitons évaluer l'utilité des modèles de perturbations vis-à-vis de la modélisation d'applications réelles et, si il y a des défaillances, voir comment adapter les modèles afin d'obtenir plus de vraisemblance tout en maintenant des propriétés algorithmiques permettant l'utilisation dans le cadre de la vérification automatique. Enfin, nous souhaitons implémenter certains les algorithmes que nous aurons développés pour une évaluation tangible de leur potentiel. Plus précisément, nous souhaitons nous intéresser aux modèles contenant des données dans des domaines infinis, comme les systèmes temporisés, hybrides, à compteurs, etc. et aux modèles à passage de message, comme les diagrammes de séquences, les systèmes à canaux et des modèles distribués plus généraux.