Model Checking Group

Details

Category: Uncategorised

Last Updated on Monday, 26 November 2012 10:03

Our main research activity focuses on Model Checking based algorithms and tools for automatic analysis and synthesis of mission or safety critical reactive systems.

A reactive system is a nonterminating system continuously exchanging information (input/output) with its environment in order to reach given goals. Examples of reactive systems are: digital hardware, control systems, operating systems, communication protocols, business processes, Decision Support Systems (DSS), Sense and Respond (SaR) systems in general.

Typically a system is considered mission critical when its failure may entail a loss of money whereas it is considered safety critical when its failure may entail loss of human lives.

Examples of mission critical systems are: space satellites, Decision Support Systems, ERP (Enterprise Resource Planning) systems. Examples of safety critical systems are: railway interlocking systems, airplanes.