Robust Development of Dependable Software Systems

The indissoluble bonds of computers and failures have produced a plurality of fault tolerant techniques to satisfy, potentially, any dependability requirement. As a consequence, the development of dependable systems is not based on inventing the mechanism that provides the desired dependability guarantees. Rather, it is based on selecting from the existing techniques the one that best meets the system's dependability requirements. Then, some codification of the selected technique can be used as the search-key for retrieving from a repository of fault tolerant mechanisms the one that implements the selected technique. Hence, the development of dependable systems becomes a process that transforms a set of dependability constraints into a fault tolerant mechanism that meets them. The focus of our work is to ensure the rigorous development of dependable systems by creating a formal basis for the aforementioned selection process. More precisely, this formal basis consists of: a system model in terms of states and actions, which permits the specification of dependability properties in temporal predicate logic; a refinement relation for dependability properties, a refinement relation for system specifications, and their correlation. a means that derives automatically the architectural impact of a dependability property to a system specification. a classification scheme, which captures the property and specification refinement relations. This scheme organizes the contents of a repository of fault tolerant mechanisms, which results in accelerating their retrieval. The practical contribution of this work is assessed in the Aster development environment. The formal basis is adapted to Aster specificities. In addition, a CASE tool is presented that uses the classification scheme to perform the analysis of dependability requirements. The CASE tool is integrated with the Aster toolkit, replacing the standard Aster tool in the retrieval of fault tolerant mechanisms. The analysis results are also used to provide guidelines for incorporating the selected fault tolerant mechanism in the system structure. While not innovative in its parts since it employs well known techniques from the fields of formal specifications, requirements analysis, software architecture, and software reuse, the originality of this work lies in the combination of existing software technologies for the benefit of system development. The development robustness is guaranteed by the rigorous analysis and the correct refinement of the system's dependability requirements