Code Slicing Tool for Effective Software Verification


KIPS Transactions on Software and Data Engineering, Vol. 4, No. 1, pp. 1-8, Jan. 2015
10.3745/KTSDE.2015.4.1.1,   PDF Download:

Abstract

Safety critical systems require exhaustive verification of safety properties, because even a single corner-case fault can cause a critical safety failure. However, existing verification approaches are too costly in terms of time and computational resource required, making it hard to be applied in practice. In this paper, we implemented a tool for minimizing the size of the verification target w.r.t. verification properties to check, based on program slicing technique[1]. The efficacy of program slicing using our tool is demonstrated in a case study with a verification target Trampoline[3], which is an open source automotive operating system compliant with OSEK/VDX[2]. Experiments have shown enhanced performance in verification, with a 71% reduction in the size of the code.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
M. Y. Park, D. W. Kim, Y. J. Choi, "Code Slicing Tool for Effective Software Verification," KIPS Transactions on Software and Data Engineering, vol. 4, no. 1, pp. 1-8, 2015. DOI: 10.3745/KTSDE.2015.4.1.1.

[ACM Style]
Ming Yu Park, Dong Woo Kim, and Yun Ja Choi. 2015. Code Slicing Tool for Effective Software Verification. KIPS Transactions on Software and Data Engineering, 4, 1, (2015), 1-8. DOI: 10.3745/KTSDE.2015.4.1.1.