A Refinement Checking Technique for Contract-Based Architecture Designs
Raphael Weber, Tayfun Gezgin, Maurice Girod · 2011
During the development of software intensive systems, typ- ically several models of this system are designed. These various models represent the system structured by different concerns, e. g. abstraction. While these approaches help to cope with complexity, the need of relating the models to one another arises. A major task is to keep model speci- fications consistent and traceable through special relations. The relation of interest for this work is the refinement relation between abstraction levels. In this work we describe a technique to check the validity of these refinement relations with respect to formal behavior/interface specifica- tions of design items. For evaluation, we apply our refinement technique to an industrial example modeled with the contract-based methodology from our previous work.