Mathematical Structures for Compositional Modeling of Reactive
Principle Investigators: Steve
Easterbrook & Marsha
Chechik, University of Toronto
Reactive Systems are formal systems that cause events in the
physical world, in reaction to a set of monitored inputs. To
say anything at all about whether such systems are safe or secure,
one has to be able to predict their behavior under the conditions
they may encounter in use. This is usually achieved by building
abstract models of the systems to study particular aspects of
their behavior. Early approaches to modeling of reactive systems
tended to ignore the internal structure of a system, treating
each system as a black box. However, structure turns out to
be important because it is often the complex interactions between
connected components of a system that lead to catastrophic failure,
and these components might originate from a number of sources,
and might be altered or replaced from time to time.
In this project, we are investigating suitable mathematical
foundations for compositional modeling, where the models of
components may be incomplete, uncertain, or inconsistent. To
develop such a foundation, we draw on our previous work on the
use of multi-valued logics for reasoning with uncertainty and
inconsistency in state machine models. We plan to explore how
to compose these models, and to reason about such compositions.
To do this, we plan to use category theory to build a framework
for structural mappings between models, with an appropriate
refinement relation over multi-valued models based on an information
order induced on the truth values of our multi-valued logics.
The expected result is a framework that shifts the emphasis
in software modeling away from a very strict "correct-by-construction"
approach, to a more explorative use of software modeling tools,
in which composition and analysis can proceed even if the component
models are incomplete and/or inconsistent.