Advantages and Limits of Formal Approaches for Ultra-High Dependability
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.
Unable to display preview. Download preview PDF.