Re-utilizing Verification Results of UML/OCL Models

Utilizing all the methods introduced in the previous chapters allows for automatically conducting various validation and verification tasks using the UML/OCL model of the system. However, once the design process enters the next stage (e.g., the implementation phase leading to a SystemC realization), most of the obtained results are not used anymore. This is unfortunate as, because of that, many checks have to be conducted again. In this chapter, we consider this problem. To this end, we first provide a case study sketching the possibilities of using verification results obtained at the UML/OCL level to lower abstraction levels. Afterwards, we even provide a formal approach that enables designers to re-utilize their verification results.