Abstract
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.
License
Topics
Session HOL-CSP_OpSem
- Introduction
- Sliding
- Throw
- Interrupt
- ReadySet
- After
- AfterExt
- AfterTrace
- Motivations
- OpSemGeneric
- OpSemFD
- OpSemDT
- AfterExtBis
- AfterTraceBis
- OpSemGenericBis
- OpSemFDBis
- OpSemDTBis
- OpSemFBis
- OpSemTBis
- NewLaws
- Conclusion
Auto-related entries
- MiniSail - A kernel language for the ISA specification language SAIL
- A Formal Development of a Polychronous Polytimed Coordination Language
- Logical Relations for PCF
- A Correctness Proof for the Volpano/Smith Security Typing System
- Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors