Contents

This set of theories presents an Isabelle/HOL+Isar formalisation of stream processing components introduces in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of the formalisation, which was elab-orated within the methodology “Focus on Isabelle”. In addition, we also applied the formalisation on three case studies that cover different application areas: process control (Steam Boiler System), data trans-mission (FlexRay communication protocol), memory and processin