Newsletter Sep21 – UCL

System Validation and Verification Eduard Baranov, UCLouvain

Correctness and security of a healthcare system developed within Serums are among the most important requirements making validation and verification tasks an essential part of the project. An additional challenge is caused by the size and complexity of the developed platform including multiple components based on various technologies.  We need to ensure that not only each component is working as intended but that the whole system does so as well. To tackle the problem, we use multiple verification approaches applied to separate components and to the complete system.

Model checking is the most common approach to guarantee the correctness of the system.  Given a model of the system in formal language with a strict semantics ensuring a single interpretation of system’s behaviour,  model checking can mathematically prove the satisfaction or violation of properties. Indeed, the approach has its limitations, most important one is computational expensiveness limiting model checking to small systems. We are using an alternative approach to avoid this limitation: a statistical model checking performs the large number of simulations on the same formal model and can ensure property satisfaction with a desired level of confidence.

Following the structure of the Serums system, the formal model is separated into smaller components, thus the properties related to a particular subsystem can be checked on the corresponding component simplifying the analysis. Resilience to malicious attacks is verified by checking properties when a model of an attacker with a possibility to interact with the system is added.

Model checking works with an abstraction of a system hiding the implementation details and, thus, working on an architectural design level. To complement the verification with the implementation checking, we are working on adoption of additional techniques based on fuzzing.  In this approach the system is tested with large number of inputs in attempt to find undesired behaviour. Inputs can be chosen randomly or by mutating previously used inputs. The latter approach allows us to focus the analysis on a particular part of the system.