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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00100064
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 10:13:49 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM

Identifiers

  • 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", Club des Enseignants et des Chercheurs en Electronique, Electrotechnique et Automatique, Section Automatique, 2004, Cachan, France. ⟨inria-00100064⟩

Share

Metrics

Record views

258