Spin with Refinement
To Run
- import project in Eclipse (with OcaIDE)
- need str,extlib libraries
- uses ocamlbuild
Usage ./spinr filename.pml
Will refine the Promela model filename.pml to a C implementation filename.pml.c
A Refinement Calculus for Promela, ICECCS 2013
End to End Verification and Validation with SPIN, CoRR 2013
Towards a Verified Cardiac Pacemaker, Technical Report NUS 2010