請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/32317
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 王凡 | |
dc.contributor.author | Jia-Fu Chen | en |
dc.contributor.author | 陳家福 | zh_TW |
dc.date.accessioned | 2021-06-13T03:42:28Z | - |
dc.date.available | 2011-07-31 | |
dc.date.copyright | 2006-07-31 | |
dc.date.issued | 2006 | |
dc.date.submitted | 2006-07-26 | |
dc.identifier.citation | [Beizer90] B. Beizer, Software Testing Techniques. Second edition. 1990
[Bugs] http://www.cnet.com/Content/Features/Dlife/Bugs/?dd [DGRV04]D. Doligez, J. Garrigue, D. Rémy, J. Vouillon. The Objective Caml system release 3.09 Documentation and user's manual Xavier Leroy”, 2004. [Hetzel88] Hetzel, William C., The Complete Guide to Software Testing, 2nd ed. Publication info: Wellesley, Mass. : QED Information Sciences, 1988. ISBN: 0894352423.Physical description: ix, 280 [Kaner93] C. Kaner, Testing Computer Software. 1993. [Kaplan00]I. Kaplan “Compiler Front End and Infrastructure Software”, May 16, 2000. [Myers79] Myers, Glenford J., The art of software testing, Publication info: New York : Wiley, c1979. ISBN: 0471043281 Physical description: xi, 177 p. : ill. ; 24 cm. [Necula05] G. Necula. CIL-Infrastructure for C Program Analysis and Transformation (v. 1.3.4), November 22, 2005 [Pan99]J. Pan, Software Testing, Spring 1999 [Rstcorp] http://www.rstcorp.com/definitions/software_testing.html [Wang03]F. Wang, Efficient Verification of Timed Automatas with BDD-like Data-Structures, Journal of STTT (Software Tools for Technology Transfer), special issue for VMCAI'2003, Preliminary version in LNCS 2575, Springer-Verlag, 2003. [Wang04a]F. Wang, Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions, 10th AMAST, Stirling, UK, July 2004, LNCS, Springer-Verlag, 2004. [Wang04b]F. Wang, Symbolic Parametric Analysis of Linear Hybrid Systems with BDD-like Data-Structures, 16th CAV, Boston, USA, July 2004, LNCS, Springer-Verlag, 2004. [Wang04c]F. Wang, F. Yu, OVL Assertion-Checking of Embedded Software with Dense-Time Semantics, RTCSA 2003, LNCS 2968, pp. 254-278, Springer-Verlag, 2004. [Wikipedia] http://en.wikipedia.org/wiki/Model_checking | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/32317 | - |
dc.description.abstract | 隨著軟體專案的越來越複雜化,相對應的測試和驗證變的越來越重要。在這篇論文中,我將提供且介紹一個軟體測試的基礎架構,在此架構中,我主要的目的是要減少測試軟體開發的成本,以增加研發的速度以及效能。在這裡我定義了一個名為分析表格(parsing tables)的中介語言,而此中介語言是可以當作程式語言和狀態機為基礎語言的橋樑。
為了要提供對軟體測試和驗證方面上多用途的功能,我們在分析表格(parsing tables)的規格上有很審慎的去定義。最後在論文的最後,將會簡單的展示一個從C 程式轉到分析表格(parsing tables)例子讓你可以更了解之間的關係。為了要達到自動化的目的,本篇論文中也提供了一個從C程式到分析表格(parsing tables)的轉譯器。 | zh_TW |
dc.description.abstract | With the explosion of the code in a project, the software testing and verification become more and more important. In this paper, our approach is to build a framework of the software verification development. In order to decrease the cost of the development, we support a parsing table as a middle language between programming language and automata-based language.
The specification of the parsing table is defined to support the multipurpose of the software verification and testing. In the last of this paper, we will show you an example from the C code to the parsing table. Furthermore, we support a parser to translate the C program into the parsing table automatically and an optimizer to optimize the parsing table for verification. | en |
dc.description.provenance | Made available in DSpace on 2021-06-13T03:42:28Z (GMT). No. of bitstreams: 1 ntu-95-R92921087-1.pdf: 588525 bytes, checksum: 43afdde12cbc2e721d5c81af4cf870ab (MD5) Previous issue date: 2006 | en |
dc.description.tableofcontents | Contents i
List of Figures iii List of Tables iv 1 Introduction 1 2 Background 4 2.1 Compiler infrastructure 4 2.2 Model checking. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Software testing. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Framework of the industrial software verification . . . . . . . . . . 13 4 Parsing table 16 4.1 Why Use Parsing Tables? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.2 An Example from C program to parsing tables . . . . . . . . . . . . . . . . . . 18 4.3 Structures of Parsing Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.3.1 File table. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.3.2 Class table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.3.3Method table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.3.4 Variable table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.3.5 Statement table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 5.1 CIL(C Intermediate Language) As Front-End. . . . . . . . . . . . . . . . . . . 29 5.2 Parser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.3 Transformation for C Program to Parsing Tables. . . . . . . . . . . . . . . . 32 5.3.1 Assignment Statement. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.3.2 Branch Statement. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6 Experiment 45 7 Related Works 46 7.1 Zephyr: Tools for a National Compiler Infrastructure. . . . . . . . . . . 46 7.2 OSUIF at UC Santa Barbara. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 7.3 Impact Research Group at the University of Illinois. . . . . . . . . . . . . 47 8 Conclusions and Future Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 Bibliography 52 Appendix A Parsing Table Flags 54 Appendix B CIL API 66 Appendix C C-API to CIL 82 | |
dc.language.iso | en | |
dc.title | 開放環境下的工業軟體驗證之編譯基礎結構 | zh_TW |
dc.title | Compiler Infrastructure for the industrial software verification in an open environment | en |
dc.type | Thesis | |
dc.date.schoolyear | 94-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 陳銘憲,黃鍾揚,王柏堯,陳俊壯 | |
dc.subject.keyword | 軟體測試,編譯結構, | zh_TW |
dc.subject.keyword | software testing,compiler infrastructure, | en |
dc.relation.page | 108 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2006-07-26 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
顯示於系所單位: | 電機工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-95-1.pdf 目前未授權公開取用 | 574.73 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。