MAFSE: A Model-Based Framework for Software Verification

Model checking techniques have been applied widely for verifying hardware designs and protocols since they can check if the system operates as desired or not without actually running the system. Recently, the usage of model checking for software verification has also been increasingly considered. One notable advantage of the model checking approach is the ability of producing counter-example when detecting undesired problem. However, model checking also suffered some prominent disadvantages which are (i) state explosion problem with non-trivial input space and (ii) over-specific model-based representation of verification results. In this paper, we propose a framework known as MAFSE (Model-based Framework for Software verification) which is still able to make full use of model checking capability for verifying software programs yet overcoming those typical drawbacks by applying appropriate methods. Our framework has been tested with some lab-scaled data and is promising to be applied for industrial software engineering.