The XBel framework has been designed for merging
and reasoning about multiple, inconsistent state machine models. XBel permits
the analyst to choose how to combine information from the multiple viewpoints,
where each viewpoint has an underlying multi-valued logic. The different
values of our logics typically represent different levels of agreement.
We have developed a multi-valued model checker,
XChek,
that allows us to check the merged model against temporal properties expressed
in CTL. XChek determines a truth value
for each property, effectively ascertaining the level of agreement for
the property. The resulting framework can be used as an exploration tool
to support requirements negotiation, by determining what properties are
preserved for various combinations of inconsistent viewpoints.
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.
2. 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.
3. 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