SPIN 2012 paper with tool demonstration appendix: Model Checking DSL-Generated C Source Code

Install
• GHC (Glasgow Haskell) compiler via haskell platform
• spin

Download:
• cablized DSLs includes MSA example
• cabalized SPINRunner
• spin runner set-up

Step 1: unzip and cabal install RulesDSL and SPINRunner (in this order)

Step 2: unzip SPINRunnerTestEnvironment.tar.gz

Step 3: Execute from shell 
        (MAC options, under cygwin replace g++ by gcc)

SPINRunner
 -c gcc -C g++
 -w PATH/SPINRunnerTestEnvironment/SrcDir
 -r PATH/SPINRunnerTestEnvironment/SPINDir
 -f PATH/SPINRunnerTestEnvironment/TestMSA.hs -t testMSA 
 -m PATH/SPINRunnerTestEnvironment/AppMSA.hs -s msa 
 -d "-DNOFAIR -DNOBOUNDCHECK -DXUSAFE" -p "-a -m1000000"

Output on standard I/O:

Number of compiled rules: 67
*** Build Promela models and generate C code:
....

Replay SPIN error traces at DSL level
Turning error_trace into a use case: Engine_Off
Executing test case Engine_Off
Turning error_trace into a use case: Engine_On1
Executing test case Engine_On1

Step 4: Interpretation of results:

Engine_Off is the LTL violated as described in the paper

Engine_On1 is some spurious failure

See 

SPINRunnerTestEnvironment/SPINDir/TestReport.html 

for explanation of matching the SPIN error traces against the LTLs.