Partenaires
Rechercher
Navigation
Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe ACADIE > Recherches
Recherches
L’équipe ACADIE a pour objectif de contribuer à l’amélioration des méthodes et outils de certification des logiciels distribués embarqués. Pour ce faire, ses thématiques de recherche se développent selon trois axes complémentaires du plus théorique au plus applicatif :
- les environnements de preuve,
- les méthodes et les langages,
- les systèmes embarqués distribués et temps réel
Environnements de preuve
Avec une expérience de co-développement de théories et de leurs formalisations en Coq qui sont publiables et partiellement publiées, on veut commencer à outiller des théories en Coq qui n’ont pas été conçues sous l’angle de leur formalisabisation. Il n’existe pas encore une implantation généralement acceptée de la théorie des catégories (en Coq, il y en a deux très complémentaires), et on vise des formalisations adaptées à nos domaines d’application. Un projet ANR en collaboration avec l’Onera a été soumis (...)
Langages et méthodes
Dans ce quadriennal, nous avons achevé certains travaux en cours concernant, d’une part les formalismes de spécification et de développement pour le temps réel et la sécurité ; et d’autre part la vérification par analyse statique de systèmes asynchrones. Ainsi, dans le contexte de la méthode B, nous avons conçu une logique temps réel pour le développement basée sur la logique MITL 03-07 [8005] (thèse de M. Rached). Cet enrichissement permet d’introduire des propriétés quantitatives au niveau des (...)
Systèmes temps réel distribués et embarqués
Historiquement, l’intérêt de l’équipe Acadie porte sur : la construction de la preuve formelle d’algorithmes distribués :prouver formellement un algorithme existant, afin de mettre en évidence des structures (de donnée ou de code) communes à une classe d’algorithmes et de faire émerger des schémas de preuve réutilisables ; le développement formel d’algorithmes distribués : partir de la spécification formelle d’un problème et le raffiner pour obtenir un algorithme implantable et garanti correct. Tout (...)