臺灣博碩士論文加值系統

程式語言擁有非常強大的能力和十分複雜的結構，因此驗證一個透過程式語言所完成的軟體將會非常困難。如果程式設計師遵循一項已經驗證過的協定來寫程式，也有可能在寫程式的過程中發生錯誤，所以對最終的程式進行驗證是很重要的。根據程式的執行流程，程式可以被視為一個具有多個程序的即時系統，而原始程式中每個獨立的片段則代表一個程序。轉譯程式將依照程式語言的文法，把程式轉譯成正規驗證模型，透過對模型的驗證，可以達成驗證程式的目的。可以對個別的程式模型進行驗證，以簡化驗證的困難度。轉譯程式的自動化是為避免在轉譯的過程中發生錯誤的可能，並把產生正規模型的過程予以簡化。我們將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 76

1.R. Alur, C. Courcoubetis, D.L. Dill, Model Checking for Real Time Systems, IEEE LICS, 1990.
2.M. Ancona, G. Dodero, V. Gianuzzi, M. Morgavi, Efficient Construction of LR(k) States and Tables, ACM TOPLAS, VOL. 13, NO. 1, pp.150-178, 1991.
3.L.L. Beck, System Software: An Introduction to Systems Programming, 2ed, Addison-Wesley, 1990.
4.J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi, UPPAAL — A Tool Suite for Automatic Verification of Real–Time Systems, in Proceedings of the DIMACS/SYCON workshop on Hybrid systems, pp. 232-243, Springer-Verlag, 1996.
5.H.K. Berg, Formal Methods of Program Verification and Specification, Prentice-Hall, 1982.
6.R.E. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Transaction on Computing, C-35(8), 1986.
7.R.E. Bryant, Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams, ACM Computing Surveys, VOL. 24, Issue 3, 1992.
8.J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic Model Checking: 1020 States and Beyond, IEEE LICS, 1990.
9.E.M. Clarke, E.A. Emerson, Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Proceedings of Workshop on Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
10.E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic Verification of Finite-state Concurrent System Using Temporal Logic Specifications: A Practical Approach, in Proceedings of the 10th ACM SIGACT-SIGPLAN, ACM Press, 1983.
11.E.M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 2000.
12.E.M. Clarke, D. Kronening, F. Lerda, A Tool for Checking ANSI-C Programs, TACAS 2004, LNCS 2988, pp. 168-176, Springer-Verlag, 2004.
13.E.M. Clarke, J.M. Wing, Formal Methods: State of the Art and Future Directions, Special ACM 50th-anniversary issue: strategic directions in computing research, ACM Computing Surveys, VOL. 28, Issue 4, pp. 626-643, ACM Press, 1996.
14.E.A. Emerson, Handbook of Theoretical Computer Science, Chapter 16, VOL. B, Elsevier, 1990.
15.E.A. Emerson, J.Y. Halpern, "Sometimes" and "Not Never" Revisited: on Branching Versus Linear Time Temporal Logic, Source Journal of the ACM, VOL 33, Issue 1, pp. 151-178, ACM Press, 1986.
16.R. Gerth, D. Peled, M. Vardi, P. Wolper, Simple On-The-Fly Automatic Verification of Linear Temporal Logic, in Proceeding PSTV 1995 Conference, Warsaw, Poland, 1995.
17.C. Heitmeyer, D. Mandrioli, Formal Methods for Real-Time Computing, Wiley, 1996.
18.T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic Model Checking for Real-Time Systems, IEEE LICS 1992.
19.G.J. Holzmann, On-The-Fly Model Checking, VOL. 28, Issue 4, ACM Computing Surveys, ACM Press, 1996.
20.G.J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, VOL. 23, NO. 5, pp. 279-295, 1997.
21.International Organization for Standardization, ISO/IEC 9899:1999: Programming languages - C, International Organization for Standardization, Geneva, Switzerland, 1999.
22.C.B. Jones, A.M. McCauley, Formal Methods - Selected Historical References, Technical Report Series UMCS-92-12-2, Department of Computer Science University of Manchester, 1992.
23.C. Kern, M.R. Greenstreet, Formal Verification in Hardware Design: a Survey, ACM Transactions on Design Automation of Electronic Systems, VOL. 4, Issue 2, pp. 123-193, ACM Press, 1999.
24.B.W. Kernighan, D.M. Ritchie, The C Programming Language, 2ed, Prentice-Hall, 1988.
25.K.G. Larsen, P. Pettersson, W. Yi, Compositional and Symbolic Model-Checking of Real-Time Systems, in Proceedings of the 16th IEEE Real-Time Systems Symposium, pp.76, IEEE Computer Society, Washington, DC, USA, 1995.
26.K.G. Larsen, P. Pettersson, W. Yi, Model-Checking for Real-Time Systems, LNCS 965, pp. 62-88, Springer-Verlag, 1995.
27.Z. Manna, A. Pnueli, Temporal Verifications of Reactive Systems: Safety, Spring-Verlag, 1995.
28.Z. Manna, A. Pnueli, Verification of Concurrent Programs: The Temporal Framework, in the Correctness Problem in Computer Science, pp. 215-273, Academic Press, London, 1981.
29.T. Mason, D. Brown, LEX and YACC, O''Reilly, 1990.
30.G.N. Naumovich, L.A. Clarke, L.J. Osterweil, Verification of Communication Protocols using Data Flow Analysis, in Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, pp. 93-105, 1996.
31.H.T. Odum, E.C. Odum, Modeling for All Scales: an Introduction to System Simulation, Academic Press, 2000.
32.A.P. Sistla, E.M. Clarke, Complexity of Propositional Linear Temporal Logics, Journal of the ACM, VOL.32, NO. 3, pp. 733-749, 1985.
33.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.
34.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.
35.F. Wang, Symbolic Parametric Analysis of Linear Hybrid Systems with BDD-like Data-Structures, 16th CAV, Boston, USA, July 2004, LNCS, Springer-Verlag, 2004.
36.F. Wang, F. Yu, OVL Assertion-Checking of Embedded Software with Dense-Time Semantics, RTCSA 2003, LNCS 2968, pp. 254-278, Springer-Verlag, 2004.
37.http://www.gnu.org/
38.http://www.uppaal.com/