### Abstract

We use a formal development for CSP, called HOL-CSP2.0, to analyse a family of refinement notions, comprising classic and new ones. This analysis enables to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles for the case of infinite sets of events. The established relations between the refinement relations help to clarify some obscure points in the CSP literature, but also provide a weapon for shorter refinement proofs. Furthermore, we provide a framework for state-normalisation allowing to formally reason on parameterised process architectures. As a result, we have a modern environment for formal proofs of concurrent systems that allow for the combination of general infinite processes with locally finite ones in a logically safe way. We demonstrate these verification-techniques for classical, generalised examples: The CopyBuffer for arbitrary data and the Dijkstra's Dining Philosopher Problem of arbitrary size.

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi
- Computer science/Semantics and reasoning

### Session CSP_RefTK

- Introduction
- Properties
- Process_norm
- CopyBuffer_props
- DiningPhilosophers
- Conclusion

### Depends on

- HOL-CSP Version 2.0

## Cite

×

CSP_RefTK-AFP

    @article{CSP_RefTK-AFP,
      author  = {Safouan Taha and Burkhart Wolff and Lina Ye},
      title   = {The HOL-CSP Refinement Toolkit},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/CSP_RefTK.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
- Jan 12, 2021 : Isabelle2020