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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: List-Infinite, Nat-Interval-Logic