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.
IWES 2017
- Details
- Category: Events
- Last Updated on Monday, 26 June 2017 10:08
MCLab organises the 2nd Italian Workshop on Embedded Systems (IWES 2017).
The workshop, which will be held in Rome on 7-8 September 2017, aims at providing the Italian community with a meeting point for the exchange of research experience in academy and industry on all aspects of embedded systems. In particular, IWES 2017 aims at:
- Providing a forum where researchers on embedded systems can present their work, exchange ideas, receive constructive feedback, and interact with the other research groups in the country, thus offering an opportunity for meeting, programming and organising projects, research work or other initiatives.
- Facilitating connections and building synergies between Academy and Industry, by providing a place where companies involved in the Embedded Systems business can showcase their current technical challenges and strategic interests and conveniently get up-to-date with the research lines and latest results achieved by the Italian research community on the topic.
- Increasing awareness of the importance of the Embedded Systems business among B.Sc., M.Sc. and Ph.D. students in Computer Science and Engineering and of the career opportunities offered by companies active in the field.
Please find out more on the IWES 2017 website.
First Summer School on Formal Methods for Cyber-Physical Systems
- Details
- Category: Events
- Last Updated on Friday, 14 July 2017 10:58
CALL FOR PARTICIPATION
1st Summer School on Formal Methods for Cyber-Physical Systems
Edition 2017: Automatic Synthesis of Controllers for Hybrid Systems
Sponsored by:
- PhD School in Natural Sciences and Engineering, University of Verona
- Department of Computer Science, University of Verona
12-16 September 2017
Department of Computer Science
University of Verona, Italy
https://cps-2017.di.univr.it/school-editions/2017
General enquiries:
This email address is being protected from spambots. You need JavaScript enabled to view it.
,
This email address is being protected from spambots. You need JavaScript enabled to view it.
,
This email address is being protected from spambots. You need JavaScript enabled to view it.
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
SyLVer
- Details
- Category: Software
- Last Updated on Wednesday, 01 February 2017 12:15
SyLVer [MicPro16,PDP15,PDP14,CAV13,SpaceOps12,DASIA11] is a software allowing System Level Formal Verification (SLFV) of Cyber Physical Systems (CPSs). SyLVer implements an assume-guarantee approach to the problem of SLFV.
The goal of SLFV 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 (HILS) based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment.
SyLVer is a stand-alone software completely running on the user premises. Furtherly, it is possible to exploit MCLab Group cloud infrastructure potential for SyLVer, by using our derived and dedicated Web-based software SyLVer as a Service (SyLVaaS). With SyLVaaS, the generation of relevant scenarios is executed in MCLab cloud infrastructure but HILS activity still takes place on the user premises (as for SyLVer), thus allowing full Intellectual Property protection on the SUV model and the user verification flow.
Introduction to QKS
- Details
- Category: Software
- Last Updated on Friday, 31 March 2017 09:54
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:
where we highlight the fact that:
- measures from plant sensors go through an Analog-to-Digital (AD) conversion (quantization) before being processed;
- the control software is typically executed by a microcontroller.
© Model Checking Group -