16 SPIN and Model-Driven Verification SPIN 4.0 introduced model-driven verification Can embed C code in a PROMELA model Code is executed as part of a transition during depth-first search SPIN compiles a PROMELA model into a C program: it's a model checker generator Embed C code in transitions by executing the compiled C code – at native speed, with real compiled behavior (including optimizations) Take advantage of all SPIN features – hashing, multicore exploration, etc.
{}