|
The
HOL-CSP
Refinement
Toolkit
Title: |
The HOL-CSP Refinement Toolkit |
Authors:
|
Safouan Taha (safouan /dot/ taha /at/ lri /dot/ fr),
Burkhart Wolff and
Lina Ye (lina /dot/ ye /at/ lri /dot/ fr)
|
Submission date: |
2020-11-19 |
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. |
BibTeX: |
@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 = nov,
year = 2020,
note = {\url{https://isa-afp.org/entries/CSP_RefTK.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
HOL-CSP |
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.
|
|