This V&V workflow intends to streamline the validity of real-time properties of the embedded systems of CardioWheel that are hard or even impossible to verify through model checking or static code analysis.

Starting from the list of requirements related with runtime and timing properties, and the system's source code, a set of formal specifications written in MARS will be defined.

A verification step of these specifications prompts the iteration of requirements, assuring that no conflicts arise.

After refining the requirements and producing a final set of specification, those specifications and the system's source code are used to run the method "Runtime Verification Based on Formal specifications" on an hardware setup that emulates the embedded systems where the final validated product is deployed.

This method returns the code definitions of the different monitors, an instrumented version of the system's code, and a report that details the findings of such monitors, either validating or finding errors/fragilities in the real time properties of the system.

With this report, a rapid step of analysis is performed, either deciding that the system is fully validated, that it needs reworking of the system's source code, or, if abnormal errors are encountered, that further requirement refinement is needed.

In parallel, a fault injection method is used to test the system's resilience to faults.