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{http://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.