Model Checking Tools for Software System Implementations

Systematic State Exploration or Model Checking techniques have been used for years to check the model of softwares against user-specified properties. Nevertheless, they never achieved a wide-spread usage because of the difficulties and problems in translating from the programming languages, which are used to develop the software, to the modeling language on which the model checker can work. Recently, there have been several efforts in direct state exploration of software system implementations. In this survey, we illustrate the challenges in this domain and explain the different solutions adopted by the state-of-the-art developed tools for state exploration of software systems. The focus of this paper in on the developed model checking tools for software systems, and it does not include solutions for unit testing and selecting the optimal test scenarios.