(18.206.238.77) 您好!臺灣時間:2021/05/12 00:42
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:王ㄙ以
研究生(外文):Szu-Yi Wang
論文名稱:即時系統驗證之正規模型的抽象化
論文名稱(外文):Abstraction of Formal Models in Real-Time System Verification
指導教授:王凡
指導教授(外文):Farn Wang
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2004
畢業學年度:92
語文別:英文
論文頁數:75
中文關鍵詞:正規模型抽象化
外文關鍵詞:formal modelabstraction
相關次數:
  • 被引用被引用:0
  • 點閱點閱:135
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
抽象化技術在驗證的過程中扮演了可能非常重要的角色。隨著安全、正確系統的需求增加,自動驗證技術的研究也就重要了起來。模型檢驗是一個有效用來自動偵測有限狀態系統是否符合其功能要求的方法。然而過程中狀態空間的迅速膨脹卻限制了其可應用的領域。抽象化的技術就是用來解決這樣一個問題的方法。給定一個系統,抽象化的技巧把它對到了另一個有著較小可能狀態空間的模型去。我們顯示了使用區間分析的方法對變數值域做抽象的結果大致上是有效的減少了狀態數量。另外,一些抽象化的基本原理也被列了出來。
Abstraction is probably the most important technique for verification. As the systems needed to convince their correctness increase, automated verification becomes a more important research. Model checking is an efficient methodology for automatically deciding if a finite state program satisfies its specification. However, state space explosion limits the applicability of it. Abstraction provides one solution to fix this problem. For a given concrete program, abstraction is a mapping such that a smaller model would obtain. We show the consequence that using interval analysis for variable abstraction may be useful to reduce much state spaces. Some principles of abstraction interpretation are also read here.
Contents


Abstract III

Chapter 1 Introduction 1

Chapter 2 Principles of Abstract Interpretation 8
2.1 Simple Examples of Abstract Interpretation 10
2.1.1 Rule of Signs 10
2.1.2 Dimension Calculus 12
2.2 Principles of Abstract Interpretation 14
2.2.1 Preliminaries 14
2.2.2 Approximation of Fixpoint Semantics Using Galois Connections 18
2.2.2.1 Galois Connections 20
2.2.2.2 Approximation of a Concrete Program Semantics with an Abstract Semantics 21
2.2.3 Widening and Narrowing 25

Chapter 3 Abstraction of Formal Models 26
3.1 Formal Models in Real-Time System Verification 28
3.2 Abstraction of Formal Models 30
3.2.1 Transition Systems and Abstraction 31
3.2.2 Approximate Abstract Models 32

Chapter 4 Variable and Operation Abstraction 35
4.1 Variable Abstraction 36
4.1.1 Interval Analysis 37
4.2 Operation Abstraction 42

Chapter 5 Algorithms of Interval Operations 45
5.1 Addition & Subtraction 45
5.2 Multiplication & Division 48
5.3 Remainder 50

Chapter 6 Implementation 53
6.1 Parsing 53
6.2 Abstraction with Interval Analysis 55
6.2.1 Grab for Bounds 56
6.2.2 Bound Transitivity 57
6.2.3 Expression Evaluation 59
6.3 An Example in Red 60

Chapter 7 Experiment 63

Chapter 8 Conclusions and Related Work 67

Appendix 68

Reference 75
Reference


[1] Constance Heitmeyer, and Dino Mandrioli. Formal Methods for Real-Time Computing. Published by John Wiley & Sons, Inc. In Chichester, New York, Brisbane, Toronto, and Singapore.

[2] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. The MIT press. Cambridge, Massachusetts, and Lodon, England.

[3] P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, Inc.

[4] P. Cousot, and R. Cousot. Abstract interpretation and application to logic programs. In B. Wegbreit. Property extraction in well-founded property sets. IEEE Transactions on Software Engineering, 1975.

[5] G. Kildall. A unified approach to global program optimization. In Conference Record of the Annual ACM, 1973.

[6] A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955.

[7] P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. In the journal of logic programming, 1992.

[8] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM, 1977.

[9] P. Cousot and R. Cousot. Systematic design of program analysis framework. ACM, 1979.

[10] P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In proceedings of the second international symposium on programming, 1976.

[11] Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM, 1999.

[12] Ramon Moore. Interval Analysis. Prentice-Hall, 1966.

[13] Neumaier. Interval methods for systems of equations. Encyclopedia of mathematics and its applications, pressed by Cambridge University, 1990.

[14] F. Wang. Red: model-checker for timed automata with clock-restriction diagram. Workshop on real-time tools, 2001.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關論文
 
系統版面圖檔 系統版面圖檔