Developing Multi-view Contracts Using Event-B and Uppaal Timed Automata

Abstract

Design-by-Contract approaches have proved essential for the development of complex cyber-physical systems with many parallel and heterogeneous components. The heterogeneity requires separation of design concerns by introducing multi-view contracts to support compositional design and verification. In some model-based development methodologies the alternative design views are supposed to be addressed by different formal methods each being most relevant to a view. In practical design the clean separation of views is not always obvious or even possible due to the dependencies and semantic overlaps between the views. Although the overlap of views introduces some redundancy, it can be turned beneficial for simplifying the design integration if explicitly addressed by the co-use of formal methods. In this paper we specify the component contracts by Event-B and Uppaal Timed Automata used respectively for behavioural and timing views and show how to combine them to merge different views in contracts. Relying on our previous results on the mapping between Event-B and Uppaal Timed Automata we extend this mapping to views of a contract and provide the verification conditions for each view separately as well as for their compatibility. We demonstrate the relevance of the approach with a Multi Robot System coordination case-study addressing the interdependencies of behavioural and timing constraints exposed in the cooperative multi-robot coverage problem.