Home
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.
PAEON (FP7-ICT-2011-9, ICT-2011.5.2)
- Details
- Category: Projects
- Last Updated on Friday, 29 May 2015 12:06
Project Title: Model Driven Computation of Treatments for Infertility Related Endocrinological Diseases
Project Acronym: PAEON
Project Website: http://paeon.di.uniroma1.it
Funding Scheme: EC Seventh Framework Programme (FP7)
- Call (part) identifier: FP7-ICT-2011-9
- Objective: ICT-2011.5.2 (Virtual Physiological Human)
- Project Type: Collaborative Project
Coordinating Person: Enrico Tronci, MCLab Sapienza University of Rome (UNIROMA1)
Project Total Funding: € 2,453,997.00
UNIROMA1 Unit Funding: € 626,382.00
SmartHG (FP7-ICT-2011-8, ICT-2011.6.1)
- Details
- Category: Projects
- Last Updated on Friday, 29 May 2015 10:33
Project Title: Energy Demand Aware Open Services for Smart Grid Intelligent Automation
Project Acronym: SmartHG
Project Website: http://smarthg.di.uniroma1.it
Funding Scheme: EC Seventh Framework Programme (FP7)
- Call (part) identifier: FP7-ICT-2011-8
- Objective: ICT-2011.6.1 (Smart Energy Grids)
- Project Type: Collaborative Project
Coordinating Person: Enrico Tronci, MCLab Sapienza University of Rome (UNIROMA1)
Project Total Funding: € 3,299,998.00
UNIROMA1 Unit Funding: € 597,378.00
Introduction to QKS
- Details
- Category: Software
- Last Updated on Thursday, 16 June 2016 14:11
QKS [TOSEM14] is a tool for automatic synthesis of correct-by-construction control software (as C code) for Discrete Time Linear Hybrid Systems. More in detail, QKS outputs a control software for software-based control systems like the following:
SyLVaaS
- Details
- Category: Software
- Last Updated on Friday, 15 July 2016 09:00
SyLVaaS [MicPro16,PDP15,PDP14,CAV13,SpaceOps12,DASIA11] is a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assume-guarantee approach to the problem of System Level Formal Verification.
The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment.
Open positions
- Details
- Category: News
- Last Updated on Thursday, 14 January 2016 11:35
We have PhD and Post-Doc positions.
For further information please contact Enrico Tronci at This email address is being protected from spambots. You need JavaScript enabled to view it. .
Tesi di Laurea Magistrale in Informatica
- Details
- Category: News
- Last Updated on Monday, 17 November 2014 16:24
Nel framework dei progetti di ricerca finanziati da ESA e dalla Comunità Europea sono disponibili tesi di laurea specialistica su algoritmi e tools per la verifica e sintesi automatica di sistemi reattivi.
Il focus attuale è Smart Grids e System Biology.
© Model Checking Group -