Rigorous Timing, Static occam, and Classic CSP: Formal Verification for IoT
Dickson Lawrence J., Martin Jeremy M.R. · IOS Press eBooks · 2019
Classic CSP is a “model without time” and yet contains time sequence and even a “time-out” or “sliding choice” operator (Roscoe, The Theory and Practice of Concurrency, 2005, p 80). The static occam language and the Transputer processor, both based on finite CSP, have time and other structure that make them a deliberate refinement of classic CSP; but occam is imperative and capable of doing completely general computing tasks. Programs written in occam and run on the Transputer can be proven correct and their behavior characterised down to cycle count. Classic CSP process descriptions of these same programs can also be investigated and proven using CSP techniques, including hiding.