跳到主要內容

臺灣博碩士論文加值系統

(44.222.64.76) 您好!臺灣時間:2024/06/16 04:42
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:鄧傑文
研究生(外文):Jei-Wen Teng
論文名稱:分散式系統之模組化驗證--方法與實例
論文名稱(外文):Modular Verification of Distributed Systems: Methods and Examples
指導教授:蔡益坤
指導教授(外文):Yih-Kuen Tsay
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:資訊管理研究所
學門:電算機學門
學類:電算機一般學類
論文種類:學術論文
論文出版年:1999
畢業學年度:87
語文別:英文
論文頁數:141
中文關鍵詞:假設/保證分散式系統模組化驗證平行組合PVS規格時間邏輯驗證
外文關鍵詞:Assumption/GuaranteeDistributed SystemsModular VerificationParallel CompositionPVSSpecificationTemporal LogicVerification
相關次數:
  • 被引用被引用:0
  • 點閱點閱:355
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:1
  一個分散式系統乃是由數個模組平行組合(Parallel Composition)而成。這類系統的模組化驗證(Modular Verification)乃在利用其他模組的規格而非程式碼,來驗證某一特定模組所須滿足的性質;然後,再由各模組所滿足的性質推導出整個系統所滿足的性質。
  一個系統的任一組成模組是以其他模組為環境的開放式系統。一個模組只有在其環境運作正常的情況下才可能滿足其應有的性質;因此,我們透過描述(1)模組的環境所須滿足的假設性質及(2)如果模組的環境遵守其假設時,模組所須滿足的保證性質,來規範(Specify)一個模組。這就是所謂模組的假設/保證式規格(Assumption/Guarantee Specification)。我們所研究的便是基於此種假設/保證式規格的模組化驗證方法。
  在這篇論文中,我們探討一個既有的基於時間邏輯的模組化驗證方法,並提出不同的表示法。我們所提出的表示法較原先的更便於應用在自動化的驗證上,雖然在手動驗證上則不如原先的簡潔。驗證軟體是一項耗時且容易出錯的工作,因此我們用一自動化驗證工具--PVS 將我們的模組化驗證方法自動化,使該方法更為實用。我們挑選三個實例來展示此自動化驗證方法的可能應用。我們也提出一方法來處理資料隱藏(Data Hiding)的問題,以避開在自動化的驗證法則中允許任意數目的量號(Quantifier)的困難。

A distributed system is the parallel composition of several modules, developed possibly by different groups. Modular Verification of such a system seeks to verify the required properties of a module using the specifications, not the codes, of other modules and then deduce properties of the entire system from properties of the modules.
Each module of a system is an open system with other modules as its environment. A module or an open system will satisfy its desire property only if its environment behaves correctly. Therefore, one specifies a module by asserting (1) assumed properties of the environment of the module and (2) guaranteed properties of the module if its environment obeys the assumption. This is the so-called assumption/guarantee specification of a module. Our modular verification method is based on such assumption/guarantee specifications.
In this thesis, we reformulate an existing modular verification method based on temporal logic. Our formulation is more convenient for mechanized analysis than the original one, though not as succinct for hand proof. As formal verification is a time-consuming and error-prone task, we mechanize our modular verification method in a well-used automated verification tool PVS to make the method more practically usable. We experiment with the mechanized method using three examples, showing its possible applications. We also introduce an approach to handle data hiding that avoids the difficulty of allowing an arbitrary number of quantifiers in mechanized verification rules.

1 Introduction 1
1.1 Background and Motivation 1
1.2 Related Work 2
1.3 Thesis Outline 3
2 Modular Specification and Verification 5
2.1 Linear-Time Temporal Logic 5
2.2 Assumption/Guarantee Specifications 7
2.3 Modular Verification Rules 8
3 Examples 13
3.1 Program KEEP_AHEAD 13
3.2 A Composed Queue 14
3.3 A Token Ring 19
4 Modular Verification in PVS 27
4.1 Formalization of Temporal Specification 27
4.2 Formalization of Modular Verification Rules 29
5 Mechanized Verification of the Examples 33
5.1 Program KEEP_AHEAd 33
5.2 A Composed Queue 36
5.3 A Token Ring 40
6 Conclusions 45
6.1 Contributions 45
6.2 Future Research 46
A Temporal Operators 47
A.1 Future Operators 47
A.2 Past Operators 48
B LTL in PVS 49
C Modular Verification Rules in PVS 51
D Specification and Proof of Program KEEP_AHEAD 53
D.1 Specification of Program KEEP_AHEAD 53
D.2 Proof of Program KEEP_AHEAD 54
D.2.1 Proof of Lemma inv_ma 54
D.2.2 Proof of Lemma inv_mb 55
D.2.3 Proof of Lemma strengthen_g 56
D.2.4 Proof of Theorem keep_ahead 56
E Specification and Proof of the Composed Queue 61
E.1 State Representation and Additional Lemmas of List
Datatype 61
E.2 Assumption/Guarantee Specification of the First
Queue 62
E.3 Assumption/Guarantee Specification of the Second
Queue 63
E.4 Assumption/Guarantee Specification of the Composed
Queue 64
E.5 Proof of the Composed Queue 66
E.5.1 Proof of Lemma inv_q2_length 66
E.5.2 Proof of Theorem composed_queue 66
F Specification and Proof of the Token Ring 73
F.1 Type Declarations and State Representation 73
F.2 Temporal Specification of the Servers Module 73
F.3 Temporal Specification of the Clients Module 74
F.4 Assumption/Guarantee Specification of the Servers
Module 75
F.5 Assumption/Guarantee Specification of the Clients
Module 78
F.6 Proof of the Token Ring 80
F.6.1 Proof of Lemma onetoken_ms 80
F.6.2 Proof of Lemma inv_mc 106
F.6.3 Proof of Theorem mutex 116
References 139

1. M. Abadi and L. Lamport. Conjoining specifications. ACM
Transactions on Programming Languages and Systems,
17(3):507-534, May 1995.
2. F. Andersen, K.D. Petersen, and J.S. Petterson. Program
verification using HOL-UNITY. Lecture Notes in Computer
Science, 780:1-16, 1994.
3. H. Barringer and R. Kuiper. Hierarchical development of
concurrent systems in a temporal logic framework. In S.D.
Brookes, A.W. Roscoe, and G. Winskel, editors, Seminar on
Concurrency, LNCS 197, pages 35-61. Springer-Verlag, 1984.
4. N. Bjorner and et al. STeP: deductive-algorithmic
verification of reactive and real-time systems. In
Proceedings of the 8th International Conference on
Computer-Aided Verification, LNCS 1102, pages 415-418.
Springer-Verlag, July 1996.
5. K.M. Chandy and J. Misra. Parallel Program Design: A
Foundation. Addison-Wesley, 1988.
6. E.M. Clarke and E.A. Emerson. Design and synthesis of
synchronization skeletons using branching time temporal
logic. In Proceedings of Workshop on Logics of Programs,
LNCS 131, pages 52-71, 1981.
7. E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional
model checking. In Proceedings of the 4th IEEE Symposium on
Logic in Computer Science, pages 353-362, 1989.
8. P. Collette. Application of the composition principle to
Unity-like specifications. In TAPSOFT '93: Theory and
Practice of Software Development, LNCS 668, pages 230-242.
Springer-Verlag, 1993.
9. J. Crow, S. Owre, J.M. Rushby, N. Shankar, and M. Srivas. A
tutorial introduction to PVS. Technical report, Computer
Science Laboratory, SRI International, Menlo Park, CA, June
1995.
10. U. Engberg, P. Gronning, and L. Lamport. Mechanical
verification of concurrent systems with TLA. In G. von
Bochmann and D.K. Probst, editors, Computer-Aided
Verification, CAV '92, LNCS 663, pages 44-55.
11. M. Gordon. HOL: A proof generating system for higher-order
logic. In G. Birtwistle and P.A. Subrahmanyam, editors,
VLSI Specification, Verification and Synthesis, pages
73-128. Kluwer, 1988.
12. O. Grumberg and D.E. Long. Model checking and modular
verification. ACM Transactions on Programming Languages and
Systems, 16(3):843-871, May 1994.
13. Z. Har'El and R.P. Kurshan. Software for analytical
development of communication protocols. AT&T Technical
Journal, 69(1):44-59, 1990.
14. B. Jonsson and Y.-K. Tsay. Assumption/guarantee
specifications in linear-time temporal logic. Theoretical
Computer Science, 167:47-72, October 1996.
15. P. Kellomaki. Verification of reactive systems using DisCo
and PVS. In J. Fitzgerad, C.B. Jones, and P. Lucas,
editors, FME'97: Industrial Applications and Strengthened
Foundations of Formal Methods, LNCS 1313, pages 589-604.
Springer-Verlag, 1997.
16. R.P. Kurshan and L. Lamport. Verification of a multiplier:
64 bits and beyond. In C. Courcoubetis, editors,
Computer-Aided Verification, CAV'93, LNCS 697, pages
166-179. Springer-Verlag, June 1993.
17. L. Lamport. The temporal logic of actions. ACM Transactions
on Programming Languages and Systems, 16(3):872-923, May
1994.
18. T. Langbacka. A HOL formalization of the temporal logic of
actions. In Higher Order Logic Theorem Proving System and
Its Applications, 7th International Workshop, 1994.
19. Z.Manna and A. Pnueli. The Temporal Logic of Reactive and
Concurrent Systems: Specification. Springer-Verlag, 1992.
20. S. Owre, N. Shankar, and J.M. Rushby. The PVS specification
language. Technical report, Computer Science Laboratory,
SRI International, Menlo Park, CA, February 1993.
21. S. Owre, N. Shankar, and J.M. Rushby. User guide for the
PVS specification and verification system. Technical
report, Computer Science Laboratory, SRI International,
Menlo Park, CA, February 1993.
22. A. Prior. Past, Present and Future. Oxford University
Press, 1967.
23. N. Shankar. Machine-assisted verification using theorem
proving and model checking. Computer and Systems Science,
158:499-528, 1997.
24. N. Shankar. Lazy compositional verification. Lecture Notes
in Computer Science, 1536:541-564, 1999.
25. N. Shankar, S. Owre, and J.M. Rushby. The PVS proof
checker: A reference manual. Technical report, Computer
Science Laboratory, SRI International, Menlo Park, CA,
February 1993.
26. Y.-K. Tsay. Compositional verification in linear-time
temporal logic. Manuscript, 1999.

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關期刊