Model-based verification is a highly successful formal method for hardware/software development. Depending on the hardware/software systems of interest, existing model-based approaches to verification use different types of mathematical models to describe abstract system behaviour, and the verification techniques they employ are tailored to these model types. However, different approaches also share certain aspects of the underlying mathematical models and of the associated verification methodologies. So far, no effort has been invested into formally relating different model-based approaches to verification. Consequently, no support is available for transferring verification methodologies between different modelling approaches, or for combining/reusing existing verification methodologies in the context of new types of models. The present project aims to address this issue, by developing the theoretical underpinnings of a modular approach to model-based verification.
Such an approach will offer several advantages, including:
(i) a unified treatment of existing modelling approaches and of their relationships,
(ii) the provision of abstraction-based verification techniques which exploit the relationships between different modelling approaches to increase the efficiency of verification,
(iii) the ability to combine/reuse existing modelling approaches/ verification methodologies when considering new classes of systems.