Inconsistency management has been defined in Finkelstein et al. [1] as the process by which inconsistencies between software models are handled so as to support the goals of the stakeholders concerned. In our opinion, software models include UML models, models expressed in a domain-specific modelling language (DSML) but also code expressed in a certain programming language. Examples of situations in which inconsistencies can arise are: in a UML model, between different UML diagrams, between the design of an application and the application code or within the application code. Violations of standards or constraints by code or design are also examples of inconsistencies.

The process of inconsistency management includes activities for detecting, diagnosing, and resolving inconsistencies. Different approaches to the detection and resolution of inconsistencies are possible. In the logic-based approach, models are expressed in some logic language. The inconsistency procedures are well-defined an have sound semantics but theorem proving is inefficient. The model checking approach translates models in a particular state-oriented language. The results of the translation are used by a model checker to detect certain inconsistencies. In a model checking approach the inconsistency detection procedures are well-defined and have sound semantics, but due to state explosion the approach is not always efficient and only specific kinds of consistency rules can be checked. Alloy tries to combine the best of both worlds: extract from a software model a relatively small number of small logical models, and check that they satisfy “the property to be proven”, i.e., the consistency. Tutorials on Alloy, an Alloy analyzer etc. are available on the Alloy website [2].

The objective of the thesis is to validate whether Alloy is suited for detecting (and resolving) different kinds of inconsistencies.

The research activities are:

1. identify a set of different inconsistencies based on a literature study and a running example
2. check whether these inconsistencies can be expressed and/or detected by Alloy
3. [if time permits] identify a possible set of resolution actions for the identified inconsistencies in step 1
4. [if time permits] check whether these resolutions can be expressed in Alloy

Niet vies zijn van logica.

[1]Finkelstein, A., Spanoudakis, G. and Till, D. Managing interference. Joint proceedings of second international software architecture workshop (ISAW-2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops. ACM Press. 1996.
[2] Alloy website : http://alloy.mit.edu