### 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).

### License

BSD License

### Topics

- Computer science/Programming languages/Language definitions

### Session FocusStreamsCaseStudies

- ArithExtras
- ListExtras
- arith_hints
- stream
- BitBoolTS
- JoinSplitTime
- SteamBoiler
- SteamBoiler_proof
- FR_types
- FR
- FR_proof
- Gateway_types
- Gateway
- Gateway_proof_aux
- Gateway_proof

## Cite

×

FocusStreamsCaseStudies-AFP

    @article{FocusStreamsCaseStudies-AFP,
      author  = {Maria Spichkova},
      title   = {Stream Processing Components: Isabelle/HOL Formalisation and Case Studies},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/FocusStreamsCaseStudies.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 18, 2013 : Isabelle2013-1