Keynote "Specification and Verification for MIMOS, our Framework for design and Update of Real-Time Embedded Systems"

Traditionally, critical software in embedded real-time systems is statically verified, and once certified supposed to remain valid for the lifetime of the system itself. Modern systems, evolving in more and more open and evolving contexts impose new requirements on embedded software. MIMOS proposes a paradigm shift to respond to these challenges by means of a combination of features: (1) it is high-level and strictly model-based concerning functional and non-functional aspects to guarantee intuitive concepts to the designer whose semantics is preserved. (2) It proposes a framework for static and dynamic (monitoring-based) verification of functionality and timing completing each other. (3) Finally, our ultimate goal is allowing to ease update of critical software. The talk will give an overview on the MIMOS concepts and the tool environment for embedded and real-time systems design developed in Uppsala within Wang Yi's ERC CUSTOMER project. Particular focus will be on the specification and verification framework that we are developing in this context.