Contents

This set of theories presents an Isabelle/HOL formalisation of stream processing components introduced in Focus, a framework for formal specification and development of interactive systems. This is an ex-tended and updated version of the formalisation, which was elaborated within the methodology “Focus on Isabelle ” [6]. 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