You are here

Mathematical Structures for Compositional Modelling of Reactive Systems

Project Type: 

This project team designed, implemented and assessed new and innovative techniques to improve the efficiency and predictive power of our simulations, hence increasing our understanding of the flow of fluid and gas.

Project Leader(s): 

Dr. Steven Easterbrook, (University of Toronto)

Reactive Systems are formal systems that cause events in the physical world, in reaction to a set of monitored inputs. Examples include control systems for aircraft, medical devices, industrial processes, and consumer appliances. In many of these examples, safety (and often security) of the system is of paramount importance. To say anything at all about whether such a system is safe or secure, one has to be able to predict its behavior under the conditions that the system may encounter in use. Unfortunately, most reactive systems are sufficiently complex that predicting their behaviour is hard. The space of possible behaviours of even relatively small systems is effectively infinite, and reasoning on the level of the detailed program code is often infeasible. In practice, we build abstract models of the systems to study particular aspects of their behavior. This modeling may be done before a system is implemented, to explore whether we have correctly understood what behaviours will be required of a proposed system, or it may be done after a system is implemented, to reason about correctness, or to predict how an existing system will behave when used in new contexts, or when modifications need to be made. Such models can be analysed using a variety of automated reasoning techniques, including model checking, theorem proving, and simulation.

Project team: 
Dr. Marsha Chechik, (University of Toronto)
Dr. Mehrdad Sabetzabeh, (University of Toronto)
Dr. Shiva Nejati, (University of Toronto)
Non-academic participants: 

Bell Canada University Labs, 
IBM Canada for Advanced Studies

Funding period: 
April 1, 2021 - March 31, 2021