Email Gateway (Mar 08 2024 at 11:08): Email Gateway (Mar 08 2024 at 11:08):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry by Benoît Ballenghien and Burkhart Wolff.
Operational Semantics formally proven in HOL-CSP
Recently, a modern version of Roscoe and Brookes Failure-Divergence Semantics
for CSP has been formalized in Isabelle (HOL-CSP) and extended (HOL-CSPM). The
resulting framework is purely denotational and, given the possibility to define
arbitrary events in a HOL-type, more expressive than the original. However,
there is a need for an operational semantics for CSP. From the latter,
model-checkers, symbolic execution engines for test-case generators, and
animators and simulators can be constructed. In the literature, a few versions
of operational semantics for CSP have been proposed, where it is assumed, of
course, that denotational and operational constructs coincide, but this is not
obvious at first glance. The present work addresses this issue by providing the
first (to our knowledge) formal theory of operational behavior derived from
HOL-CSP via a bridge definition between the denotational and the operational
semantics. In fact, several possibilities are discussed. As a bonus, we have
defined three new operators: Sliding, Throw and Interrupt which are of
particular pragmatic interest in operational semantics. Moreover, we have proven
new laws for HOL-CSP improving the latter.
https://www.isa-afp.org/entries/HOL-CSP_OpSem.html
Enjoy,
René
Last updated: Apr 28 2024 at 20:16 UTC