Cléopatre

Projet AtlanSTIC - 2006
Analyse formelle de propriétés de systèmes d’exploitation
temps réels à base de composants :
Application au système Cléopatre

Coordonnateurs : Christian Attiogbé (LINA/COLOSS),
Thibault Garcia-Fernandez(IRCCyN/STR)
Contact : Christian Attiogbé / Christian.Attiogbe(@)univ-nantes.fr
Avril 2006

Participants

Equipe Composants et logiciels sûrs - COLOSS/LINA
Equipe Systèmes temps réel - STR/IRCCyN

Description

La sûreté de fonctionnement des composants logiciels est un paramètre déterminant pour la qualité des systèmes qui intègrent ces composants. Les composants logiciels se retrouvent au niveau des applications ou au niveau des services de base (systèmes d’exploitation de ressources diverses).
Nous proposons d’étudier dans ce projet la validation de noyaux de systèmes d’exploitation temps réels par la vérification à priori des propriétés de correction en vue d’envisager la sûreté de fonctionnement lorsque de tels noyaux-systèmes sont enfouis dans des équipements divers.
Cléopatre (Composant Logiciel sur Etagères Ouverts Pour Applications Temps Réel Embarqués), un système d’exploitation temps réel, sert ici de cadre pour l’étude.

But du projet

Le but du projet est précisément d’assurer le fonctionnement correct (sans défaillances) de composants du système Cléopatre. Un composant Cléopatre est une collection de primitives qui fournissent des services aux applications temps réel et/ou à d’autres composants.
Il s’agit de mettre au point des méthodes et techniques de validation des composants implantés dans ce système d’exploitation et d’étendre ces méthodes au cadre plus général des systèmes à micro-noyaux. Nous posons ainsi les bases d’une plateforme (logicielle) de validation de systèmes bâtis à l’aide de composants interchangeables.

Contexte du projet et verrous scientifiques

Le cadre de ce projet est l’emploi des méthodes formelles pour la validation de systèmes logiciels en particulier les composants logiciels du système Cléopatre.
La part du logiciel dans les domaines de la domotique, de l’automobile, de l’avionique, du nucléaire et de l’aérospaciale est de plus en plus importante. Dans ce contexte, le logiciel dit "temps réel embarqué" est placé sous le contrôle de systèmes d’exploitation dont la sûreté de fonctionnement est un paramètre primordial à cause des enjeux humains, matériels et financiers.
CLEOPATRE est un système d’exploitation temps réel embarqué construit avec une collection de composants ouverts (interfaces publiques et codes sources accessibles). Il est bâti au dessus du système LINUX. Il intègre des fonctionnalités liées à l’ordonnancement temps réel, la gestion de ressources critiques, l’exécution de tâches critiques ou non, périodiques ou non. Les composants de Cléopatre sont interchangeables ; selon les applications, le concepteur peut choisir les composants à intégrer dans son système d’exploitation. Cléopatre vise à être un système d’exploitation embarqué ; par exemple, être implanté dans les dispositifs de contrôle ou de pilotage d’équipements physiques divers tels que des appareils domestiques, des robots, etc.
Ce faisant, il y a nécessité de s’assurer de son fonctionnement, au moins en ce qui concerne les modules identifiés comme critiques.

Les méthodes formelles sont utilisées pour le développement de systèmes fiables et aussi pour l’analyse des propriétés (vérification formelle) de ces systèmes. Les méthodes formelles requièrent l’élaboration de modèles adéquats qui représentent le plus fidèlement possible les systèmes à étudier.
L’étape initiale d’une étude à l’aide des méthodes formelles est une modélisation mathématique du système à développer ou à analyser.
Les langages de spécification formelle permettent de construire de tels modèles. Généralement, les propriétés analysées sont les propriétés de sûreté (safety) et les propriétés de vivacité (liveness). Les propriétés de sûreté permettent de s’assurer qu’aucun fonctionnement anormal ne peut arriver ; les propriétés de vivacité garantissent que le système évolue (afin d’effectuer ses fonctionnalités). La correction d’un système est donc examinée principalement via ces propriétés.
On distingue aussi deux grandes catégories de techniques d’analyse formelle :
_les techniques de preuve de théorèmes (theorem-proving) ; ici le modèle est utilisé comme un système de déduction. Les propriétés attendues du système sont exprimées comme des théorèmes qu’il faut alors prouver à partir du système de déduction. Ces techniques sont le plus souvent utilisées pour l’analyse des propriétés de surêté mais sont aussi applicables pour les propriétés de vivacité.
_les techniques de vérification de modèles (model-checking) ; ici un modèle correspond à une abstraction du système qu’on aurait à l’exécution ; c’est un automate à états. On exprime ensuite dans un formalisme logique (souvent temporel), les propriétés souhaitées du système et on montre que le modèle (automate à état) satisfait les propriétés. On explore alors chacun des états pour s’assurer que le système possède bien les propriétés.

Le raisonnement priviliégié dans les deux cas est un raisonnement logique et symbolique. Moyennant une modélisation appropriée et une formalisation des propriétés souhaitées, on peut envisager d’analyser tout système.

Les verrous scientifiques auxquels nous nous attaquons dans ce projet relèvent :
_du défi de la modélisation mathématique de systèmes complexes (c’est-à-dire non triviaux quant à leur description et leur développement),
_la preuve de propriétés de systèmes à composants interchangeables constitue un problème ouvert lié à la propriété de compositionnalité,
_la validation des systèmes embarqués de façon générale est une préoccupation majeure qui vise à rassurer les utilisateurs des systèmes et rationaliser les processus de développement.

Présentation du projet et organisation

Les systèmes d’exploitation temps réel modernes sont composés d’un micro-noyau et de modules qui complètent les fonctionnalités du système. Ces modules sont par conséquent critiques et doivent être corrects, c’est-à-dire exempts de fautes ou de mauvais fonctionnements. Cela peut et doit être établi formellement.
Un plan d’étude consiste à construire un modèle formel d’un module pour prouver qu’il a les propriétés voulues. Ensuite, lorsque le système évolue (par ajout ou modification de modules), on doit s’assurer que certaines propriétés globales sont maintenues au niveau du système et d’autres propriétés maintenues au niveau des modules.
On peut ainsi s’assurer de la conservation des propriétés de correction de systèmes d’exploitation lorsqu’on y ajoute/modifie des modules.
Notamment dans le cadre de notre étude avec Cléopatre, nous assimilons un module à un composant. Nous considérons alors l’ajout de composants dans le système Linux temps réel.
A partir d’expériences sur des composants système, avec une architecture spécifique, nous visons un cadre de vérification plus général. Les vérifications seront effectuées avec la possibilité de modifier, soit les composants à tester, soit les propriétés à vérifier.
Le projet va s’organiser autour de différents aspects énumérés ci-dessous. Nous appelons ici contexte, une collection de composants sélectionnés que l’on va intégrer pour assurer des fonctionnalités précises ; certains composants du contexte peuvent être ainsi remplacés par d’autres, ayant des fonctionnalités identiques mais différents dans leur réalisation.
1. Etude d’une approche de modélisation des composants (utilisés dans les systèmes d’exploitation) permettant d’analyser leur intégration dans le système global : modélisation des composants et expression de leurs propriétés.
2. Modélisation formelle du contexte que l’on souhaite étudier et expression des propriétés relatives ; les propriétés attendues des différents composants.
3. La preuve de la correction d’un contexte. Ici nous allons exprimer les propriétés globales désirées pour un contexte puis prouver leur satisfaction. Nous nous appuierons sur la méthode B (preuve de théorèmes) et les outils CADP ou Spin (évaluation de modèles) pour effectuer des analyses multifacettes. Dans un premier temps nous allons expérimenter les méthodes de vérification de modèles pour étudier les composants qui serviront dans l’expérimentation puis nous étendrons au contexte. Les techniques de preuve de théorèmes seront utilisées de façon complémentaire.
4. Pour faire face à l’aspect interchangeabilité, nous allons explorer les techniques de bissimulation. A première approximation, un composant est bissimilaire à un autre s’il a un comportement équivalent. Ensuite on tiendra compte de la spécificité des composants (différence d’algorithmes, différence de performances, etc).
5. Généralisation des techniques et des méthodes. Au fur et à mesure et à l’issue des étapes présentées ci-dessus, on dégagera des techniques génériques et des méthodes systématiques (sous forme de règles) afin de généraliser notre étude et de pouvoir l’appliquer à plus de modules.

Résultats escomptés

_Validation de quelques composants de Cléopatre.
_Elaoration de techniques et méthodes de vérification adaptées à la structuration du sytème Cléopatre.
_Un prototype d’environnement générique de validation de système : ce prototype mettra en oeuvre des étapes de traitement paramétré par des composants et leurs propriétés.

	Cléopatre Projet AtlanSTIC
Cléopatre Accueil Telechargements Documentations Applications Vision temps réel Bras manipulateur Plateforme mobile Projets Projet original Projet AtlanSTIC	Projet AtlanSTIC - 2006 Analyse formelle de propriétés de systèmes d’exploitation temps réels à base de composants : Application au système Cléopatre Coordonnateurs : Christian Attiogbé (LINA/COLOSS), Thibault Garcia-Fernandez(IRCCyN/STR) Contact : Christian Attiogbé / Christian.Attiogbe(@)univ-nantes.fr Avril 2006 Participants Equipe Composants et logiciels sûrs - COLOSS/LINA Equipe Systèmes temps réel - STR/IRCCyN Description La sûreté de fonctionnement des composants logiciels est un paramètre déterminant pour la qualité des systèmes qui intègrent ces composants. Les composants logiciels se retrouvent au niveau des applications ou au niveau des services de base (systèmes d’exploitation de ressources diverses). Nous proposons d’étudier dans ce projet la validation de noyaux de systèmes d’exploitation temps réels par la vérification à priori des propriétés de correction en vue d’envisager la sûreté de fonctionnement lorsque de tels noyaux-systèmes sont enfouis dans des équipements divers. Cléopatre (Composant Logiciel sur Etagères Ouverts Pour Applications Temps Réel Embarqués), un système d’exploitation temps réel, sert ici de cadre pour l’étude. But du projet Le but du projet est précisément d’assurer le fonctionnement correct (sans défaillances) de composants du système Cléopatre. Un composant Cléopatre est une collection de primitives qui fournissent des services aux applications temps réel et/ou à d’autres composants. Il s’agit de mettre au point des méthodes et techniques de validation des composants implantés dans ce système d’exploitation et d’étendre ces méthodes au cadre plus général des systèmes à micro-noyaux. Nous posons ainsi les bases d’une plateforme (logicielle) de validation de systèmes bâtis à l’aide de composants interchangeables. Contexte du projet et verrous scientifiques Le cadre de ce projet est l’emploi des méthodes formelles pour la validation de systèmes logiciels en particulier les composants logiciels du système Cléopatre. La part du logiciel dans les domaines de la domotique, de l’automobile, de l’avionique, du nucléaire et de l’aérospaciale est de plus en plus importante. Dans ce contexte, le logiciel dit "temps réel embarqué" est placé sous le contrôle de systèmes d’exploitation dont la sûreté de fonctionnement est un paramètre primordial à cause des enjeux humains, matériels et financiers. CLEOPATRE est un système d’exploitation temps réel embarqué construit avec une collection de composants ouverts (interfaces publiques et codes sources accessibles). Il est bâti au dessus du système LINUX. Il intègre des fonctionnalités liées à l’ordonnancement temps réel, la gestion de ressources critiques, l’exécution de tâches critiques ou non, périodiques ou non. Les composants de Cléopatre sont interchangeables ; selon les applications, le concepteur peut choisir les composants à intégrer dans son système d’exploitation. Cléopatre vise à être un système d’exploitation embarqué ; par exemple, être implanté dans les dispositifs de contrôle ou de pilotage d’équipements physiques divers tels que des appareils domestiques, des robots, etc. Ce faisant, il y a nécessité de s’assurer de son fonctionnement, au moins en ce qui concerne les modules identifiés comme critiques. Les méthodes formelles sont utilisées pour le développement de systèmes fiables et aussi pour l’analyse des propriétés (vérification formelle) de ces systèmes. Les méthodes formelles requièrent l’élaboration de modèles adéquats qui représentent le plus fidèlement possible les systèmes à étudier. L’étape initiale d’une étude à l’aide des méthodes formelles est une modélisation mathématique du système à développer ou à analyser. Les langages de spécification formelle permettent de construire de tels modèles. Généralement, les propriétés analysées sont les propriétés de sûreté (safety) et les propriétés de vivacité (liveness). Les propriétés de sûreté permettent de s’assurer qu’aucun fonctionnement anormal ne peut arriver ; les propriétés de vivacité garantissent que le système évolue (afin d’effectuer ses fonctionnalités). La correction d’un système est donc examinée principalement via ces propriétés. On distingue aussi deux grandes catégories de techniques d’analyse formelle : _les techniques de preuve de théorèmes (theorem-proving) ; ici le modèle est utilisé comme un système de déduction. Les propriétés attendues du système sont exprimées comme des théorèmes qu’il faut alors prouver à partir du système de déduction. Ces techniques sont le plus souvent utilisées pour l’analyse des propriétés de surêté mais sont aussi applicables pour les propriétés de vivacité. _les techniques de vérification de modèles (model-checking) ; ici un modèle correspond à une abstraction du système qu’on aurait à l’exécution ; c’est un automate à états. On exprime ensuite dans un formalisme logique (souvent temporel), les propriétés souhaitées du système et on montre que le modèle (automate à état) satisfait les propriétés. On explore alors chacun des états pour s’assurer que le système possède bien les propriétés. Le raisonnement priviliégié dans les deux cas est un raisonnement logique et symbolique. Moyennant une modélisation appropriée et une formalisation des propriétés souhaitées, on peut envisager d’analyser tout système. Les verrous scientifiques auxquels nous nous attaquons dans ce projet relèvent : _du défi de la modélisation mathématique de systèmes complexes (c’est-à-dire non triviaux quant à leur description et leur développement), _la preuve de propriétés de systèmes à composants interchangeables constitue un problème ouvert lié à la propriété de compositionnalité, _la validation des systèmes embarqués de façon générale est une préoccupation majeure qui vise à rassurer les utilisateurs des systèmes et rationaliser les processus de développement. Présentation du projet et organisation Les systèmes d’exploitation temps réel modernes sont composés d’un micro-noyau et de modules qui complètent les fonctionnalités du système. Ces modules sont par conséquent critiques et doivent être corrects, c’est-à-dire exempts de fautes ou de mauvais fonctionnements. Cela peut et doit être établi formellement. Un plan d’étude consiste à construire un modèle formel d’un module pour prouver qu’il a les propriétés voulues. Ensuite, lorsque le système évolue (par ajout ou modification de modules), on doit s’assurer que certaines propriétés globales sont maintenues au niveau du système et d’autres propriétés maintenues au niveau des modules. On peut ainsi s’assurer de la conservation des propriétés de correction de systèmes d’exploitation lorsqu’on y ajoute/modifie des modules. Notamment dans le cadre de notre étude avec Cléopatre, nous assimilons un module à un composant. Nous considérons alors l’ajout de composants dans le système Linux temps réel. A partir d’expériences sur des composants système, avec une architecture spécifique, nous visons un cadre de vérification plus général. Les vérifications seront effectuées avec la possibilité de modifier, soit les composants à tester, soit les propriétés à vérifier. Le projet va s’organiser autour de différents aspects énumérés ci-dessous. Nous appelons ici contexte, une collection de composants sélectionnés que l’on va intégrer pour assurer des fonctionnalités précises ; certains composants du contexte peuvent être ainsi remplacés par d’autres, ayant des fonctionnalités identiques mais différents dans leur réalisation. 1. Etude d’une approche de modélisation des composants (utilisés dans les systèmes d’exploitation) permettant d’analyser leur intégration dans le système global : modélisation des composants et expression de leurs propriétés. 2. Modélisation formelle du contexte que l’on souhaite étudier et expression des propriétés relatives ; les propriétés attendues des différents composants. 3. La preuve de la correction d’un contexte. Ici nous allons exprimer les propriétés globales désirées pour un contexte puis prouver leur satisfaction. Nous nous appuierons sur la méthode B (preuve de théorèmes) et les outils CADP ou Spin (évaluation de modèles) pour effectuer des analyses multifacettes. Dans un premier temps nous allons expérimenter les méthodes de vérification de modèles pour étudier les composants qui serviront dans l’expérimentation puis nous étendrons au contexte. Les techniques de preuve de théorèmes seront utilisées de façon complémentaire. 4. Pour faire face à l’aspect interchangeabilité, nous allons explorer les techniques de bissimulation. A première approximation, un composant est bissimilaire à un autre s’il a un comportement équivalent. Ensuite on tiendra compte de la spécificité des composants (différence d’algorithmes, différence de performances, etc). 5. Généralisation des techniques et des méthodes. Au fur et à mesure et à l’issue des étapes présentées ci-dessus, on dégagera des techniques génériques et des méthodes systématiques (sous forme de règles) afin de généraliser notre étude et de pouvoir l’appliquer à plus de modules. Résultats escomptés _Validation de quelques composants de Cléopatre. _Elaoration de techniques et méthodes de vérification adaptées à la structuration du sytème Cléopatre. _Un prototype d’environnement générique de validation de système : ce prototype mettra en oeuvre des étapes de traitement paramétré par des composants et leurs propriétés.