Aimed Contribution

This project aims to contribute to safer medical cyber-physical systems. This contribution will be structured along two main axes: a medical systems axis, and a Verification & Validation (V&V) axis.

On the system’s axis we will develop appropriate modelling strategies, for both the systems and the requirements, considering both model checking and theorem proving approaches.

On the V&V axis we will investigate the most appropriate techniques for the verification of the requirements and models identified in the above axis.

We will develop techniques to speed up model checking and improve the quality of verification results, by incorporating user preferences and knowledge about the domain into the analysis. Using know-how from the team in both prototyping single devices and ambient assisted living environments, rapid prototyping approaches based on formal methods will be developed to help communicate the results of the verification.

To address how the requirements are met by code running in the relevant devices, we will investigate the difficult issue of how high-level properties, expressed at the level of models, can be mapped to code-level properties, to enable the use of a software model checking tool.