Model Checking DSL-Generated C Source Code

We report on the application of SPIN for model-checking C source code which is generated out of a textual domain-specific language (DSL). We have built a tool which automatically generates the necessary SPIN wrapper code using (meta-)information available at the DSL level. The approach is part of a larger tool-chain for developing mission critical applications. The main purpose of SPIN is for bug-finding where error traces resulting from SPIN can be automatically replayed at the DSL level and yield concise explanations in terms of a temporal specification DSL. The tool-chain is applied in some large scale industrial applications.

• Type: Journal
• Year: 2012
• Where: SPIN
• Authors: Martin Sulzmann, Axel Zechner
• Keywords: C Source Code, Concise Explanations, SPIN 2012, Textual Domain, Theoretical Computer Science