Email Gateway (Jan 12 2021 at 12:10): Email Gateway (Jan 12 2021 at 12:10):From: Manuel Eberl <eberlm@in.tum.de>
The HOL-CSP Refinement Toolkit
by Safouan Taha, Burkhart Wolff, and Lina Ye
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.
https://www.isa-afp.org/entries/CSP_RefTK.html
Enjoy!
Manuel
smime.p7s
Last updated: Jan 04 2025 at 20:18 UTC