期刊名称：International Journal of Security and Its Applications
印刷版ISSN：1738-9976
出版年度：2013
卷号：7
期号：3
出版社：SERSC
摘要：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.
