Dependeability evaluation of object-oriented systems (DEVOS)

Sponsors:

Hungarian-Italian Intergovernmental S & T Cooperation Programme for 2000-2002

Period:

2000-2002

Project leader:

András Pataricza, Ph.D. (DMIS BUTE, Budapest, Hungary)
Prof. Andrea Bondavalli (CNUCE-CNR, Pisa, Italy)

Participants:

István Majzik, György Csertán, András Petri, Gábor Huszerl (BUTE DMIS)
Diego Latella, Felicita DiGiandomenico, Fabrizio Grandoni, Andrea Coccoli (CNUCE-CNR, PDCC)

Project aim:

Good implementation of systems (especially those supporting critical applications) alone does not assure that a proper quality of service will be delivered by the system in operations. From the very early stages of the design process, an early validation of concepts and architectural choices (without wasting time and resources in the realization phase) is essential to understand whether the required quality of service will be delivered. Dependability (covering reliability, availability, safety) is one of the parameters to be validated, especially in systems required to provide continuous and/or critical services.
The use of formal methods for the validation of properties is one methodological improvement of the system production process. However, the need of the knowledge of sophisticated mathematical formalisms and techniques prevented the wide adaptation of formal methods. Our approach hides the background mathematics for the designer by (i) providing a set of transformations from the high-level visual model to the formal model and (ii) automatic back-annotation of the results. In this way, by methodological or automatic derivation of formal models we contribute in making the dependability evaluation by application of formal methods more a discipline than an art.

This research originates from the ESPRIT LTR project Nr. 27439 HIDE (High-Level Integrated Design Environment for Dependability). HIDE aimed at the extension of modern design methodologies of object-oriented software by model-based mathematical analysis and validation. UML (Unified Modeling Language) was adopted as a standard of object-oriented development and the analysis of the UML-based model was provided by a set of transformations from the engineering visual models to mathematical models. The partners were involved in the analysis of dependability attributes through stochastic modeling and formal verification.
The project proved the feasibility of the approach. However, the resource constraints during the feasibility study imposed to develop methods with severe constraints on the designer and restricted the usable UML elements to a well-defined subset. Moreover, only the fundamental concepts of the design were taken into account and subtle modeling problems were not addressed (e.g. fault activation process without explicit repair and recovery, concurrency without synchronous communication etc.). The extension of the model class covered by the methods is required in order to be able to apply them to practical systems. Applications built in standard frameworks for dependable software, like Fault Tolerant CORBA, offer themselves as ideal testbed for the evaluation of these new methods.
The following subtasks are going to be elaborated:

• Stochastic modeling for dependability
• Formal verification
• Case studies in the framework of the Fault Tolerant CORBA

Further information:

András Pataricza, Ph.D.