Model Checking Laboratory

Sapienza Model Checking Lab carries out research on methods and software tools for analysis and design of safety and mission critical systems.

In such a framework, within the healthcare context we focus on methods and software tools to support "In Silico Trials", that is simulation based assessment of safety and efficacy of drugs and biomedical devices. This is done by developing, through collaborations with multidisciplinary research teams, computational models for: human (patho-) physiology (Virtual Patients, VP), drug administration strategies (therapies), safety and efficacy criteria.

The therapy and the VP form a "closed loop control system" where the therapy plays the role of the controller and the VP that of the controlled system ("plant"). Safety and efficacy criteria provide Key Performance Indicators (KPIs) for the therapy (controller).

Through AI and Model checking based techniques we generate a cohort of VPs representing phenotypes of the (real) patients on which we want to assess safety or efficacy of the therapy. Then, using AI and model checking driven simulation approaches we assess safety and efficacy by looking for worst case values for safety and efficacy criteria (KPIs).

The above approach has been successfully applied in the framework of the European project PAEON coordinated by MCLab.

We are now working on general purpose tools (e.g., SBML2Modelica) based on the available mechanistic models of human cells as well as of the immune system.

Building on such experiences we are now developing methods and tools to support In Silico trials for Covid-19 vaccines and therapies. Those are based on computational models for physiology as well as of the immune systems.