AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics

David Trachtenherz

February 23, 2011

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize the AutoFocus Semantics (a time-synchronous subset of the Focus formalism) as stream processing functions on finite and infinite message streams represented as finite/infinite lists. The formalization comprises both the conventional single-clocking semantics (uniform global clock for all components and communications channels) and its extension to multi-clocking semantics (internal execution clocking of a component may be a multiple of the external communication clocking). The semantics is defined by generic stream processing functions making it suitable for simulation/code generation in Isabelle/HOL. Furthermore, a number of AutoFocus semantics properties are formalized using definitions from the IntervalLogic theories.


BSD License


Session AutoFocus-Stream