Information for Prospective Students:
Profs. Chechik and Easterbrook are looking for several students to assist us with building front-end of our multi-valued model-checker and with conducting case studies. Here is a list of potential projects:
1. Development of a good modelling language for our model-checker.
Currently, the language of the model-checker describes a graph, with its states and transitions between them. The goal of this project is to produce a formal yet usable language (e.g., like Promela or the language of SMV) that allows specification and composition of non-trivial multi-valued models.
2. Interfacing our model-checker with commercial model-building tools such as UML.
The idea of this project is to enable reasoning with inconsistencies and negotiation for UML models. The project involves building a converter between UML statecharts (and potentially other types of diagrams) and the input language of our model-checker, and interpretation of counter-examples in the original UML models. Further, we may be interested in other front-ends for domain-specific reasoning.
Information from different stakeholds can be merged in a variety of ways. We have identified a number of them in our work. This project entails implementation of the different merge operations (synchronous and asynchronous composition, partial/total systems, etc.) on models expressed in the language of our model-checker. A more complex task is integrating merges with the "more usable" language of the model- checker defined in Project 1. Another more complex task is using the different merges in the domain-specific framework to help negotiation.
4. Case studies.
We have produced a number of simple case studies to assess effectiveness of our framework. We are now ready to work on realistic case studies together with our industrial partners. In particular, we are looking for people interested in conducting case studies in: