Mots Clés
|
|
Résumé
Ce projet s'adresse aux systèmes embarqués critiques de grande taille, pour lesquels la réutilisation devient un problème crucial. Le projet a pour objectif l'étude d'un atelier intégré pour le développement et l'utilisation de composants embarqués sûrs. L'usage d'un langage adéquat contribuant pour une large part à la sûreté des systèmes informatiques, nous privilégions ici une approche ``langage'' des aspects suivants:- support au cycle de vie, depuis les phases initiales de spécification jusqu'au code embarqué efficace ;
- mécanismes de composition modulaires utilisables aussi bien dans les programmes, dans leurs spécifications, dans la description des environnements;
- validation précoce des assemblages de composants;
- validation précoce du comportement dynamique des systèmes par simulation des programmes et des spécifications, tout au long des phases de développement; la possibilité d'exécuter des programmes incomplets est un des objectifs prioritaires.
L'approche proposée consiste à bâtir un ensemble de langages, et leurs outils associés, sur un socle sémantique commun.
Nous choisissons le modèle mathématique synchrone, qui fournit une sémantique simple de la concurrence et du temps. Il a été utilisé avec succès dans la définition de langages et outils industriels (e.g, Scade, Sildex, Esterel) pour la programmation de systèmes de contrôle/commande critiques. Il permet déjà, dans un cadre unifié, de décrire et composer programmes et propriétés. Il est suffisamment général pour décrire d'autres modèles de concurrence (en particulier asynchrones) et combiner des objets déterministes et non-déterministes.
Nous définirons dans ce cadre commun un ensemble de langages pour : la programmation, la spécification des programmes et des environnements, la description des assemblages, les propriétés des assemblages.
Par ailleurs nous étudierons l'application de méthodes de validation de manière très précoce dans le cycle de vie : validation des assemblages, validation d'un composant pour un environnement donné, etc. Nous proposons de formuler ces nouveaux problèmes de validation en termes exploitables par les techniques de vérification existantes, et de prévoir une interface de l'atelier avec les outils existants.
Le projet s'appuie sur les compétences des équipes du projet dans les domaines de la programmation synchrone ; de la sémantique et de l'implantation de langages pour les systèmes embarqués ; des outils de validation et de simulation de systèmes.
