王凡臺灣大學：電機工程學研究所蔡麟讚Cai, Lin-ZanLin-ZanCai2007-11-262018-07-062007-11-262018-07-062005http://ntur.lib.ntu.edu.tw//handle/246246/53004RED整合CRD的技術和HRD的技術而成為能處理時間自動機和線性混合自動機之圖像式TCTL樹狀時態邏輯檢證/模擬工具。為了要將RED能處理稠密時間系統及線性混合系統的圖像式驗證技術分享出去，並發展出RED更多的應用方式，以及提供一個更有彈性且更具效率的正規模型建構途徑，我們著手開發RED的函式庫介面：REDLIB。並且在這篇論文中，以用JAVA寫成之全新的電子寵物商店範例JPetStore為例進行實驗，展示如何以REDLIB來建構出正規模型和發展出更多之應用可能。RED(Region-Encoding Diagram) is an integrated symbolic TCTL model-checker/simulator for timed automata with CRD (Clock-Restriction Diagram) technology and linear hybrid automata with HRD (Hybrid-Restriction Diagram) technology. In order to share the symbolic verification technology of RED for dense-time systems and linear hybrid systems, develop more other applications on RED, and provide a more flexible and efficient way of formal method construction. We construct the library interface of RED, REDLIB, and do an experiment with JPetStore which is a completely new implementation of Pet Store demo application written in Java. This experiment demonstrates how to use REDLIB to construct verification applications.Contents i List of Figures iii List of Tables iv Acknowledgements v Chinese Acknowledgements vi Abstract vii Chinese Abstract viii 1 Introduction 1 2 Formal Verification of Embedded Systems with RED 4 2.1 Overview . . . . . . . . . . . . . . . . . .. . 4 2.2 Technological Bckground . . . . . . . . . . . . 5 2.3 Utilization of RED . . . . . . . . .. . . . . . 9 3 REDLIB: The Library Interface of RED 16 3.1 Application Program Interface of REDLIB . . . . 17 3.2 Methods of Library Interface Construction . . . 19 3.3 Model Construction with REDLIB . . . . . . . . . 21 4 The Introduction of JPetStore 28 4.1 Background . . . . . . . . . . . . . . . . . . . 28 4.2 Function Feature . . . . . . . . . . . . . . . . 30 4.3 Architecture of JPetStore . . . . . . . . . . . 31 5 Experiment 34 5.1 Modeling The Behavior of Function . . . . . . . 34 5.2 Formal Model Construction of JPetStore . . . . . 35 5.3 Advantages of REDLIB . . . . . . . . . . . . . . 36 5.4 Experimental Result . . . . . . . . . . . . . . 42 6 Related Works 44 6.1 CUDD . . . . . . . . . . . . . . . . . . . . . . 44 6.2 NuSMV . . . . . . . . . . . . . . . . . . . . . 45 7 Conclusions and Future Works 47 A Installation of JPetStore with MySQL and Tomcat on Windows computer 49 B The JPetStore Model in RED Syntax 53 C The Parameters of Setting JPetStore Model 64 Bibliography 66460113 bytesapplication/pdfen-US驗證模型檢驗正規模型函式庫嵌入式系統電子寵物商店verificationmodel checkingformal modellibraryembedded systemJPetStorethesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53004/1/ntu-94-R92921105-1.pdf