Rigorous Timing, Static occam, and Classic CSP: Mathematical Ground Truth
Dickson Lawrence J., Martin Jeremy M.R. · IOS Press eBooks · 2019
This Fringe presentation will continue the comparison of the two approaches from our first talk (“Formal Verification for IoT”) in rigorous mathematical detail. We introduce the mathematical concept of a Covering-with-Boundary (CwB), prove the equivalence of cycle-counted occam on a Transputer with this path diagram, and proceed to prove cases that avoid both divergence and effective divergence by finite restrictions. Due to static characteristics of occam-and-Transputer-based “Ground Truth,” we are also able to prove Hardware-Software Equivalence, and reach IoT conclusions that extend to non-digital payloads.