Synthèse formelle par raffinement de modèles et de logiciels pour l'automaisation

Dominique Méry 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Ce document présente la modélisation incrémentale et prouvée de systèmes intégrant des parties logicielles. La technique de modélisation repose sur un langage simple à base d'événements, sur un langage de propriétés de sûreté et d'invariance, sur une relation entre les modèles appelée raffinement de modèles et sur des conditions de vérification associées aux modèles. Cette technique de développement de modèles est répandue dans les méthodes formelles comme B, TLA, UNITY, Actions Systems, Refinement Calculus, \ldots Nous donnons une description brève de la méthode appelée B événementiel et nous montrons sur un exemple simple comment une telle méthode peut être mise en oeuvre et rendue effective pour le cas de systèmes d'automatisation. Notre exemple est simple et est emprunté à d'autres auteurs qui ont utilisé d'autres méthodes mais illustre l'intérêt de l'intégration du raffinement dans le développement de systèmes. Il s'agit d'essai de modélisation en situation d'une étude de cas.
Type de document :
Communication dans un congrès
Journées d'Etude "Automatique et Informatique", 2004, Cachan, France, 2004
Liste complète des métadonnées

https://hal.inria.fr/inria-00100064
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:49
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00100064, version 1

Collections

Citation

Dominique Méry. Synthèse formelle par raffinement de modèles et de logiciels pour l'automaisation. Journées d'Etude "Automatique et Informatique", 2004, Cachan, France, 2004. 〈inria-00100064〉

Partager

Métriques

Consultations de la notice

235