Safety properties based scenario generation for model checking trampoline OS

Model checking has proven to be a successful technology to verify real-time embedded and safety-critical systems. However an application of model checking in practice still requires manual construction of an environment model, which has a direct impact on verification cost. This paper suggests an automated scenario generation technique through a property-based static analysis of function-call relationship of the program source code. We present the scenario generation process and show application results on the Trampoline operating system using CBMC as a back-end model checker. The experimental result shows that our approach is able to reduce the verification cost significantly in terms of memory space and run time.