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]. Once inconsistency are detected the question arises how these inconsistencies can be fixed and how to determine which fixes are applicable. In [3] possible inconsistency resolutions are generated and proposed to the user. In their related work they claim that Alloy could also be used to generate changes that resolve inconsistencies.

The objective of the thesis is to validate the usage of Alloy to generate changes for resolving inconsistencies in UML design methods based on [3].

The thesis activities are:

1. identify a set of different inconsistencies based on a literature study and a running example
2. use Alloy to generate different changes resolving inconsistencies based on the approach presented in [3]
3. implement the approach in our tool support RACOoN which is an Eclipse plug-in allowing the detection of different UML inconsistencies.

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
[3]Egyed, A. and Letier, E. and Finkelstein, A., Generating and Evaluating Choices for Fixing Inconsistencies in UML Design Models, 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), To appear. 2008.