A Framework for Multi-Valued Reasoning over Inconsistent Viewpoints
Abstract
During requirements elicitation, different stakeholders often hold
different (and incompatible) views of how the proposed system
should behave, resulting in inconsistencies between their
descriptions. Consensus may not be needed for every detail, but it
can be hard to determine whether a particular disagreement affects
the critical properties of the system. Existing viewpoints-based
frameworks support detection and resolution of inconsistencies,
but do not support reasoning about the properties of inconsistent
models. In this paper, we describe the XBel framework 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.