Stream Processing Components: Isabelle/HOL Formalisation and Case Studies

Title:	Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
Author:	Maria Spichkova (maria /dot/ spichkova /at/ rmit /dot/ edu /dot/ au)
Submission date:	2013-11-14
Abstract:	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 extended and updated version of the formalisation, which was elaborated within the methodology "Focus on Isabelle". In addition, we also applied the formalisation on three case studies that cover different application areas: process control (Steam Boiler System), data transmission (FlexRay communication protocol), memory and processing components (Automotive-Gateway System).
BibTeX:	@article{FocusStreamsCaseStudies-AFP, author = {Maria Spichkova}, title = {Stream Processing Components: Isabelle/HOL Formalisation and Case Studies}, journal = {Archive of Formal Proofs}, month = nov, year = 2013, note = {\url{http://isa-afp.org/entries/FocusStreamsCaseStudies.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
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.