Functional analysis for safe and available system design

In this article, we address the problem of the design of safe and available complex systems, based on a functional analysis. We propose a formal theory of such a design in terms of refinement calculus and Markov modelling techniques. Based on this approach, we succeed in reflecting the well known fact that increasing the safety level of a system induces decreasing its availability. We are then able to highlight some methodological guidelines for a proof oriented system specification theory for safe and available systems.