Rechercher

Systèmes Sûrs

Groupes

Evenements

ICFEM 2015 - The 17th International Conference on Formal Engineering Methods

Since 1997, ICFEM has been serving as an international forum for researchers and practitioners...
03-11-2015 au 07-11-2015 - Cnam

1st International Workshop about Sets and Tools (SETS 2014)

Affiliated to ABZ 2014 international conference The workshop aims at bringing together...
03-06-2014 - Toulouse, France

Description

L’équipe « Systèmes Sûrs » consacre ses recherches à la spécification, la conception, la vérification et l’évaluation des systèmes, en particulier des applications critiques du point de vue de la sûreté et de la sécurité. L'objectif est de développer des méthodes, techniques et outils permettant d'énoncer les propriétés recherchées pour des applications et de démontrer que ces applications satisfont les propriétés attendues. Toutes les recherches menées dans notre équipe rentrent dans le cadre général des méthodes formelles. Nos activités s'articulent autour de deux axes principaux : l’axe « Conception et Programmation Raisonnée » (CPR) et l’axe « Vérification et Evaluation de Systèmes Parallèles et Asynchrones » (VESPA).

Autour de l’axe CPR, les activités de l'équipe se situent généralement à la frontière entre la recherche fondamentale et la recherche appliquée. En effet, un des objectifs principaux de ces travaux est de pemettre la conception et la vérification des programmes réalistes et, pour cela, nous développons des méthodes et des outils pour produire des logiciels sûrs. Ces méthodes reposent essentiellement sur des techniques sémantiques et déductives qui, pour une part importante, s’appuient sur la théorie des types et plus précisément l'assistant à la preuve Coq.

Un des challenges pour cette communauté est de faire adopter plus amplement les méthodes formelles au niveau industriel, et ceci nécéssite d’abord un haut degré d'automatisation et ensuite la production d'interfaces non seulement faciles à utiliser mais aussi proches des habitudes des développeurs et de leurs processus de développement. Pendant cette période, nous avons donc cherché à maintenir un équilibre autour de la plateforme Focalize et de la preuve de correction d'outils et d'algorithmes avec Coq, en intégrant toutefois une orientation nouvelle vers la verification d’algorithmique répartie. L'aspect lié au développement de techniques de preuve interactive et de déduction automatique a aussi été central et faforisé par la collaboration avec l'équipe Inria Deducteam.

Les travaux conduits autour de l’axe VESPA portent principalement sur le développement et l'utilisation de méthodes formelles pour la spécification, la vérification  et l'évaluation de systèmes informatiques (matériels & logiciels) et réseaux d'information et de  communication en focalisant sur les questions de partage (ou conflit), de concurrence, de coordination (interaction), de reconfiguration (mobilité), de qualité de service (QdS), de réactivité (contraintes temps réel) et de commande (contrôle) qui sont fortement liées entre elles.

Une approche naturelle pour maîtriser la complexité de ces systèmes consiste à les concevoir en termes d'assemblages de composants communicants (de manière généralement asynchrone). Le terme « composant » étant compris comme une unité de conception (et de réutilisation) et peut recouvrir plusieurs appellations telles que sous-programme, objet, module, agent, capteur, processus, thread, service, etc...

Les formalismes mathématiques permettant de décrire la structure, la composition, l’évaluation (qualitative et quantitative) de tels systèmes ainsi que leur évolution sont :  les réseaux de Petri et leurs extensions (RdP temporisés et stochastiques), la logique de réécriture et son prolongement la logique des tuiles, les algèbres de processus, les systèmes réactifs bigraphiques (BRS) ainsi que les langages de description architectures logicielles (ADL).

collaboration

Collaboration avec : Lab. Veriform de Ecole Polytechnique de Montréal (Canada) et Institute of Computing University of Campinas (Brésil), UC2 (Algérie)