Modular approach to model based verification

One way to ensure the correctness of hardware/software systems is by using so-called model-based verification techniques in their development. The application of such techniques involves describing the abstract behaviour of systems by means of mathematical models, and subsequently using these models to explore/validate system behaviour, and to verify correctness properties of systems, formulated in a suitable mathematical language. The advantage of model based verification is that, once an abstract model of a system has been provided, the task of validating/verifying system behaviour can be performed by a computer.Both the mathematical models and the mathematical languages currently used in model-based verification were designed for specific types of hardware/software systems. Much effort has, for instance, been invested into the modelling and verification of non-deterministic systems (i.e. systems whose evolution may follow more than one path), and of probabilistic systems (i.e. systems whose evolution can only be predicted with a certain probability). However, little support has been provided for reusing/combining existing verification techniques, in order to model and verify other kinds of systems. New mathematical models and corresponding mathematical languages have to be developed from scratch every time a different type of system needs to be considered. This is highly impractical, since often the new types of systems combine features already treated in existing models (e.g. non-deterministic and probabilistic behaviour). Thus, the availability of techniques which allow existing models/languages and the corresponding verification techniques to be combined/reused in new contexts would prove extremely valuable.A promising approach towards addressing this issue is the use of so-called coalgebraic models in describing abstract system behaviour. Coalgebraic models generalise the existing mathematical models for state-based systems. Moreover, the coalgebraic framework allows relationships between different mathematical models to be made precise. As a result, coalgebraic models provide the right setting within which to unify existing verification methodologies, and to facilitate their reuse.This project will develop a framework which allows existing mathematical models and the associated mathematical languages to be treated uniformly, relationships between different models/languages to be made precise, and verification techniques to be combined/reused in order to efficiently verify new types of hardware/software systems.