Semantic structures and logic properties of computer-based system dependability cases

This work addresses the issue of structuring the validation process of dependable computer based systems. It is motivated by the desire to make the licensing and certification of these systems more reliable and efficient. The paper analyses the structural, semantic and logic properties of the demonstration that an embedded computer-based system is adequately specified, designed and maintained in operation. Three basic classes of dependability claims are identified. Claims which address (i) the environment-system interface: (ii) the design: and (iii) the operational behaviour. To deal with the disparity of the real domains, models and languages in which these three classes of claims are formulated and supported, a structure is proposed to analyse the relations between classes and the convergence of arguments based on the diverse sources of evidence. The properties of models and languages required for the interpretations of the real domains and the proof obligations are identified. The implications of these properties on design criteria and mechanisms are discussed. A real dependability case is used to illustrate the concepts and discuss their applicability.