Mathematics of Information Technology and Complex Systems


Homepage
 
Project Highlights
 
Milestones
 
Research
 
Team Members
 
Partner Organizations
 
Students
 
Publications
 
Presentations
 
Events
 
MITACS Home
 

Mathematical Structures for Compositional Modeling of Reactive Systems

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.