A Methodology for Verifying Refinements of Partial Models

By: Rick Salay, Marsha Chechik, Michalis Famelis, Jan Gorzny

Abstract

Models are typically used for expressing information that is known at a particular stage in the software development process. Yet, it is also important to express what information a modeler is still uncertain about and to ensure that model refinements actually reduce this uncertainty. Furthermore, when a refining transformation is applied to a model containing uncertainty, it is natural to consider the effect that the transformation has on the level of uncertainty, e.g., whether it always reduces it. In our previous work, we have presented a general approach for precisely expressing uncertainty within models. In this paper, we use these foundations and define formal conditions for uncertainty reducing refinement between individual models and within model transformations. We describe tooling for automating the verification of these conditions within transformations and describe its application to example transformations.

Keywords

Partial Models, Uncertainty, Refinement, Model Transformation

Cite as:

Rick Salay, Marsha Chechik, Michalis Famelis, Jan Gorzny, “A Methodology for Verifying Refinements of Partial Models”, Journal of Object Technology, Volume 14, no. 3 (August 2015), pp. 3:1-31, doi:10.5381/jot.2015.14.3.a3.