C2 – Composition and Abstraction with Explications

A typical embedded device maintains and periodically updates a behaviour model of its surrounding world, on which it bases its decisions. In full generality, this model encompasses aspects of time, costs, resource consumption, randomness, continuous dynamics, and epistemic uncertainty and knowledge. In order to construct, guarantee and explicate properties of such devices, as well as of families thereof, this project attacks key semantic, algorithmic and technical challenges arising in this context, with a prime focus on compositionality and abstraction. The project works with natural yet abstract representations of all of the above aspects. Our vision is to establish and exploit the principles of composition and abstraction for stochastic systems involving hybrid dynamics and cost parametrisation, to arrive at an effective cause-effect analysis framework based on quantitative summaries of component characteristics, in the form of component inserts and supported by abstract argumentation for explications at runtime.