Regresar

A compositional scheme and framework for safety critical systems verification

Abstract:

Safety-Critical Systems (SCS)must satisfy dependability requirements such as availability, reliability, and real-time constraints, in order to justify the reliance of the critical service they deliver. A verification framework named Formal Compositional Verification Approach (FCVA) is presented here. FCVA establishes a compositional method to verify safety, fairness and deadlock absence of SCS. Software components of a given critical system are model-checked to verify the aforementioned properties. Our objective in this paper is to facilitate the design of an SCS from a collection of verified simpler components, and hence allowing complete complex SCS software verification. An application on a real-life project in the field of mobile phone communication is discussed to demonstrate the applicability of FCVA.