Proof-Oriented Fault-Tolerant Systems Engineering : Rationales, Experiments and Open Issues

Gérard Morel 1 Dominique Méry 2 Jean-Baptiste Léger Thierry Lecomte
1 CRAN - Centre de Recherche en Automatique de Nancy
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Proving system properties such as fail-safety is a challenge for systems engineering since industrial automation is nowadays embedding intensive on-site and remote infotronics components engineered with increasing intuitive ease-of-use techniques. Since a formal proof of the complete safe-behaviour of the resulting ad-hoc system is not possible, this paper argues that Proof Oriented Systems Engineering formal techniques should bridge the gap with Fault Tolerant Systems Engineering practical techniques in order to mathematically check the proof of fail-safety. Rationales, experiments and open issues are addressed on combining the formal B event-based method using the B proof assistant with a technical-safety modelling formalized-framework.
Keywords : méthode formelle safe-process. automation engineering automatique ingénierie formelle fault-tolerant systems engineering formal methods proof-oriented fail-safe systems engineering
Type de document :
Communication dans un congrès
7th IFAC Symposium on Cost Oriented Automation - COA'2004, 2004, Gatineau, Québec, Canada. 2004
Liste complète des métadonnées
https://hal.inria.fr/inria-00100068
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-00100068, version 1

Collections

INRIA | CRAN | UNIV-LORRAINE | LORIA

Citation

Gérard Morel, Dominique Méry, Jean-Baptiste Léger, Thierry Lecomte. Proof-Oriented Fault-Tolerant Systems Engineering : Rationales, Experiments and Open Issues. 7th IFAC Symposium on Cost Oriented Automation - COA'2004, 2004, Gatineau, Québec, Canada. 2004. 〈inria-00100068〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

206

Contact


archive-ouverte@inria.fr