Advantages and Limits of Formal Approaches for Ultra-High Dependability

  • Marie-Claude Gaudel
Part of the ESPRIT Basic Research Series book series (ESPRIT BASIC)


This paper discusses the advantages and limits of formal approaches to software development for achieving ultra-high dependability of critical computer systems. It is a companion paper to Paper VI.G on the validation of ultra-high dependability for software systems. Among the issues to be addressed here, are: what is a formal specification, what can be done with it, what is correctness, what kind of certainty comes from a proof, and from testing? The paper does not claim to answer these questions: rather it is a formulation of the author’s reflections in this area.


Formal Method Formal Approach Deduction System Formal Verification Code Activity 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© ECSC — EC — EAEC, Brussels — Luxembourg 1995

Authors and Affiliations

  • Marie-Claude Gaudel
    • 1
  1. 1.LRI, CNRS et Université de Paris-SudFrance

Personalised recommendations