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

 Title: AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics Author: David Trachtenherz Submission date: 2011-02-23 Abstract: 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. BibTeX: @article{AutoFocus-Stream-AFP, author = {David Trachtenherz}, title = {AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics}, journal = {Archive of Formal Proofs}, month = feb, year = 2011, note = {\url{https://isa-afp.org/entries/AutoFocus-Stream.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Nat-Interval-Logic Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.