工業計畫軟體模型的抽象化

Automatic Abstraction of C Programs for the Verification of Industrial Projects

邱仁尉(Ren-Wei Qiu)

指導教授 ： 王凡

國立臺灣大學/電機資訊學院/電機工程學研究所/碩士(2006年)

https://doi.org/10.6342/NTU.2006.10356

摘要

軟體驗證越來越重要，特別是對某些重要目的程式以及複雜的系統。因為這些程式太複雜，驗證工具幾乎沒有完善的支援。為驗證這些系統， 我們必須首先對他們做抽象化的運算。經過抽象化的產出將可被應用於model checking, test case generation or simulation等等的技術上。抽象化系統可以被工程師或是由程式自動完成。如果是利用工程師來完成抽象化的工作，將會造成大量的時間及金錢上的成本。為了避免時間及金錢上的成本浪費，由程式自動完成抽象化的工作將是一個選擇。而本篇論文便是以自動化完成抽象化的方式來實作。其產出將可以被應用在其它的驗證軟體上。

關鍵字

抽象化

並列摘要

Software verification is more and more important, especially some critical purpose programs and complicated systems. Since these programs are too complicated, barely verification tools can support them. For verifying these systems, we have to abstract them first. This throughput would be used to model checking, test case generation or simulation. The work that abstract systems can be realized by programmers or automatically. If this work is accomplished by programmer, we should take more time to train programmers than past. Because this way would take too cost to train programmers, we have to achieve this work automatically to save money and time. The main purpose of this paper is to realize software abstraction automatically and effectively. The output of our work would be the middle code for verification tools.

並列關鍵字

abstraction

參考文獻

[1] F. Tip. A survey of program slicing techniques. Journal of Programming Lan-guages, 3:128-189, 1995.

[2] F. Wang. Formal Veri‾cation of Timed Systems: A Survey and Perspective. Pro-ceedings of the IEEE, Vol. 92, NO. 8, Aug. 2004.

[3] F. Wang. E±cient Veri‾cation of Timed Automata with BDD-like Data-Structures. Journal of Software Tools for Technology Transfer (STTT), Springer-Verlag, Vol. 6, NO. 1, Jul. 2004.

[5] F. Wang, Pao-Ann Hsiung. E±cient and User-Friendly Veri‾cation. IEEE Trans-actions on Computers, Vol. 51, NO. 1, ITCOB4, ISSN 0018-9340, Jan. 2002.

[9] T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In SIGPLAN Conference on Programming Language Design and Implementation, pages 203V213, 2001.