|
|
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.
3. Merges.
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:
|
|
|
