From informal to formal modeling

Any software model should be consistent and correct at some point in the development process. And there are many tools for this, including our preferred approach.  But this doesn’t mean all models should be correct from the very beginning. More the opposite, in early stages of the development process we may want to let the models go loose to facilitate the exploration of design alternatives without having to worry about creating perfect models all the time.

This is one of the reasons that explain why so many designers end up modeling with PowerPoint or other drawing tools. But then, we don’t have the chance to verify those models ever. Unless we redraw them from scratch in a formal modeling tool.

So how can we get the best of both worlds?. How to use a formal modeling tool but relax the quality constraints until we want to enforce them?. In the paper: Towards Facilitating the Exploration of Informal Concepts in Formal Modeling Tools presented at Modevva’21 we discuss our ideas for applying informal ideas for model development within a formal tool.

The basic idea is to relax the requirements expressed with particular modeling language elements and allow developers to dynamically customize the level of formality in a visual and intuitive way. In particular, we propose a metaphor that can be used to introduce flexibility in a formal modeling tool and to let developers control and adjust the desired level of (in)formality in their models. The degree of (in)formality is presented as a set of sliders (see the example below) controlled by the developer, providing a visual and intuitive representation. We illustrate how this metaphor can be incorporated in the USE specification environment for selected modeling features.

Thanks to this slider metaphor, developers can relax the formality requirement and take advantage of verification and validation in scenarios of early prototyping, design space exploration or model evolution. For example, suppose that the developer decides that an integrity constraint should be temporarily considered as a soft constraint, i.e., instantiations that violate the constraint are tolerated. In that case, the model finder (the component for constructing instantiations conformant to the model) should switch its behavior from satisfiability (try to fulfill all constraints) to max-satisfiability (try to fulfill all hard constraints and as many soft constraints as possible). Furthermore, the developer could aim for even more diverse constraints and test what type of instantiations are produced if the integrity constraint is ignored during the model finding process by setting the slider accordingly.

Besides, it also enables developers to operate with “informal” models and iteratively increase the level of formality until a final model is reached. Overall, we believe that this proposal improves the user experience of formal modeling tools, creating new usage scenarios. User experience is an open challenge in modeling tools and this proposal could contribute to improving it.

Modeling elements candidates for relaxation

Our proposal for handling (in)formality is generic, nevertheless, we now turn to show how it can be realized in USE in which the level of formality of a UML and OCL model can be relaxed according to several perspectives. We have considered the semantics and realization of relaxing the following language features:

1. Class typing: Flexible class typing refers to the ability to define and use objects of an unknown, undecided or purposely undefined type during validation. On the UI, the slider ALL controls the introduction of a most general class Object for representing objects effectively without type. A slider on position Generous for a single classes expresses that any attribute or any role resulting in this respective class can be substituted with an untyped object from class Object.
2. Attribute typing: The attribute value may be taken from OclAny or Collection(OclAny) for collection-valued attributes. An attribute slider controls this option.
3. Role typing: Untyped role substitution may become possible by lifting associations to the most general class Object and by explicitly controlling the role substitution with a slider. Not necessarily all associations have to be lifted (as done in our example), some associations and roles may remain “exactly” typed.
4. Multiplicity satisfaction: In every single association, through sliders, lower bounds may be decreased and upper bounds may be increased. Switching between single-valued (0..1, 1) and multi-valued (e.g., 0.._*, 1.._*) multiplicities may lead to the fact that an OCL constraint cannot be evaluated which will be reported to the developer. Manipulating “High” and “Low” both change the numerical range setting, e.g., from 0 to 1 to 2. “Low” will always stay under “High”.
5. Constraint satisfaction: We provide three settings in the sliders for constraints: (1) ‘Enforced’ for a usual hard constraint that is always satisfied; (2) ‘Soft’ for a constraint that is satisfied only if that is possible; relevant in cases when our Model Validator automatically constructs object models; ‘Relaxed’ completely ignores the constraint.

We propose to have combined relaxation control (ALL) for all elements in each single group. Furthermore, we suggest an overall relaxation control for the complete model. For larger models a manageable grouping mechanism must be established, e.g., it will be unpractical to handle all attributes (as we have done in our toy example) as a single group. Relaxation control for language elements must be grouped by class and/or package.

Regarding correctness, intuitively each slider either removes a conformance requirement of object diagrams with respect to class diagrams (e.g., satisfying integrity constraints) or sets a weaker requirement (e.g., less restrictive multiplicities).

Embedding of relaxation into the development process

In a practical development process,  one wants to start with a high degree of informality and in an iterative process achieve more and more formal descriptions. We have here taken first the former view (from formal to informal), because we wanted to point out that informal models can be achieved when working in a formal modeling tool. The tool support that we envision has to ensure that the latter (from informal to formal) is made possible by offering the right tool options.

Our overall aim with relaxation is to improve the development process. We want to facilitate iterative development steps that lead from loose (class) models to sharper ones (e.g., with iteratively introduced integrity constraints, sharp multiplicities and more specialized object, attribute and role types). A high degree of flexibility for developers should enable them to let their ideas flow without tool complaints, e.g., about missing or unsatisfied typing details. Support for development with imperfect, even inconsistent intermediate models contributes to flexibility as well. Qualified tool feedback through automatic object model construction for checking implications of design decisions should be supported as well.

As future work, we plan to implement this feature in USE. Moreover, we are interested in computing the least informal setting that should be selected in order to tolerate a set of instantiations of interest, as this information highlights potential issues. Finally, we want to look into supporting the relaxation of other modeling elements, such as whole-part relationships or operation contracts.