王凡臺灣大學：電機工程學研究所邱仁尉Qiu, Ren-WeiRen-WeiQiu2007-11-262018-07-062007-11-262018-07-062006http://ntur.lib.ntu.edu.tw//handle/246246/53498軟體驗證越來越重要，特別是對某些重要目的程式以及複雜的系統。因為這些程式太複雜，驗證工具幾乎沒有完善的支援。為驗證這些系統， 我們必須首先對他們做抽象化的運算。經過抽象化的產出將可被應用於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.Contents i List of Figures iii Acknowledgements v 1 Introduction 1 2 The Abstraction Framework of Industrial Software 3 2.1 The General Abstraction Framework of Industrial Software . 3 2.2 The Five Modules of Our Abstraction . . . . . . . . . . . . 5 3 Parsing tables 8 3.1 The Parsing Tables in Array Form . . . . . . . . . . . . . 8 3.1.1 File Table . . . . . . . . . . . . . . . . . . . . . . . 9 3.1.2 Class Table . . . . . . . . . . . . . . . . . . . . . . 10 3.1.3 Procedure/method Table . . . . . . . . . . . . . . . . . 11 3.1.4 Variable Table . . . . . . . . . . . . . . . . . . . . . 13 3.1.5 Statement Table . . . . . . . . . . . . . . . . . . . . 14 3.2 The Parsing Tables in Link List Form . . . . . . . . . . . 16 3.2.1 File Table . . . . . . . . . . . . . . . . . . . . . . . 17 3.2.2 Class Table . . . . . . . . . . . . . . . . . . . . . . . 17 3.2.3 Procedure/method Table . . . . . . . . . . . . . . . . . 18 3.2.4 Variable Table . . . . . . . . . . . . . . . . . . . . . 19 3.2.5 Statement Table . . . . . . . . . . . . . . . . . . . . 21 4 Abstraction 23 4.1 typedef Elimination . . . . . . . . . . . . . . . . . . . 23 4.2 Abstracting Library-calls . . . . . . . . . . . . . . . . 24 4.3 Abstracting Variable . . . . . . . . . . . . . . . . . . 32 4.3.1 Interval Analysis . . . . . . . . . . . . . . . . . . 33 5 Implementation 40 5.1 The Data Structure for Parsing Tables . . . . . . . . . . 40 5.1.1 File Table . . . . . . . . . . . . . . . . . . . . . . . 41 5.1.2 Class Table . . . . . . . . . . . . . . . . . . . . . . 41 5.1.3 Procedure/method Table . . . . . . . . . . . . . . . . 42 5.1.4 Variable Table . . . . . . . . . . . . . . . . . . . . 42 5.1.5 Statement Table . . . . . . . . . . . . . . . . . . . 44 5.2 The Implementation of The Five Modules . . . . . . . . 46 5.2.1 Input Module . . . . . . . . . . . . . . . . . . . . 46 5.2.2 Data Structure Transformation Module . . . . . . . . 47 5.2.3 Library-calls Abstraction Module . . . . . . . . . . 51 5.2.4 Variable Abstraction Module . . . . . . . . . . . . . 55 5.2.5 Output module . . . . . . . . . . . . . . . . . . . . 60 6 Experimental Results 61 6.1 Input Module . . . . . . . . . . . . . . . . . . . . . 61 6.2 typedef elimination . . . . . . . . . . . . . . . . . . 61 6.3 Library-calls abraction . . . . . . . . . . . . . . . . 67 6.4 Variable Abstraction Module . . . . . . . . . . . . . . 69 7 Conclusions and Related Work 71 Bibliography 731347918 bytesapplication/pdfen-US抽象化abstractionthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53498/1/ntu-95-R93921108-1.pdf