王凡臺灣大學：電機工程學研究所王立德Wang, Lih-derLih-derWang2007-11-262018-07-062007-11-262018-07-062004http://ntur.lib.ntu.edu.tw//handle/246246/53093程式語言擁有非常強大的能力和十分複雜的結構，因此驗證一個透過程式語言所完成的軟體將會非常困難。如果程式設計師遵循一項已經驗證過的協定來寫程式，也有可能在寫程式的過程中發生錯誤，所以對最終的程式進行驗證是很重要的。根據程式的執行流程，程式可以被視為一個具有多個程序的即時系統，而原始程式中每個獨立的片段則代表一個程序。轉譯程式將依照程式語言的文法，把程式轉譯成正規驗證模型，透過對模型的驗證，可以達成驗證程式的目的。可以對個別的程式模型進行驗證，以簡化驗證的困難度。轉譯程式的自動化是為避免在轉譯的過程中發生錯誤的可能，並把產生正規模型的過程予以簡化。我們將C語言程式透過自動轉譯程式，轉譯成時間自動機的模型，而模型本身是用Red的語法來描述。General purpose programming languages are rich in functionalities and therefore have complicated structures. Hence verifying software programs written in such programming languages can be very difficult. Even if the technical specifications had been verified to be error-free, there may still be errors introduced by the actual implementation. It is important that the verification is performed on the final program. Based on the work flow, a program can be considered as a real-time system with many processes, where each process is represented by a fragment of the original program. According to the grammars of the specific programming language, an automated translator can be used to translate the programs into corresponding formal verification models. The whole program can then be verified by applying the standard verification techniques to each model individually. The automation of translation can simplify the task of creating a formal model and identify potential errors in the implementation. We will present our implementation of a program that translates basic C programs into timed automata described by Red.Chapter 1 Introduction 1 Chapter 2 Automated Verification 5 2.1 Concurrent Systems 6 2.2 Temporal Logic 8 2.3 BDD 12 2.4 Timed Automata 14 2.5 Red Verification Tool 17 Chapter 3 From Programming Language to Timed Automata 21 3.1 Lexical Analyzer 21 3.2 Parser 23 3.3 Intermediate Structure 27 3.4 Model Generation 28 Chapter 4 Implementation 31 4.1 Tools 31 4.2 Data Structure 35 4.2.1 Node 35 4.2.2 Stack and list 36 4.3 Mode Generation Rules 36 Chapter 5 Experiment 43 5.1 Experiment 43 5.2 Discussions 47 Chapter 6 Related Works 51 6.1 UPPAAL 51 6.2 CBMC 52 6.3 TC 53 6.4 Spin 55 Chapter 7 Conclusions and Future Works 57 Bibliography 59 Appendix 63 A.1 The Grammar of C Programming Language 63 A.2 The Definitions of Terminal Tokens in Flex 72 A.2.1 Constant 72 A.2.2 Identifier 72 A.2.3 Reserved words 72 A.2.4 Operators 72 A.3 The Definitions of Non-terminal Tokens 73 A.4 The Declarations of Data Structures in Translator 73 A.5 The definitions of flags 74 A.5.1 decl_rec.spec flag definition 74 A.5.2 stat_rec.spec flag definition 76718581 bytesapplication/pdfen-US自動驗證轉譯程式時間自動機Timed AutomataAutomated VerificationTranslatorthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53093/1/ntu-93-R91921085-1.pdf