(3.237.20.246) 您好!臺灣時間:2021/04/15 10:01
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:蔡麟讚
研究生(外文):Lin-Zan Cai
論文名稱:嵌入式系統驗證函式庫之建立:以電子寵物商店進行實驗
論文名稱(外文):Library Construction for Embedded System Verification: An Experiment with JPetStore
指導教授:王凡
指導教授(外文):Farn Wang
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2005
畢業學年度:93
語文別:英文
論文頁數:69
中文關鍵詞:驗證模型檢驗正規模型函式庫嵌入式系統電子寵物商店
外文關鍵詞:verificationmodel checkingformal modellibraryembedded systemJPetStore
相關次數:
  • 被引用被引用:1
  • 點閱點閱:155
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
RED整合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 66
[1]E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, A. Rasse. Data-Structures for the Verification of Timed Automatas. Proceedings, HART''97, LNCS 1201, Springer-Verlag.
[2]R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems.IEEE LICS, 1990.
[3]R. Alur, C.Courcoubetis, T.A. Henzinger, P.-H. Ho. Hybrid Automata: an Algorithmic Approach to the Specification and Verification of Hybrid Systems. Proceedings of HYBRID''93, LNCS 736, Springer-Verlag, 1993.
[4]R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP'' 1990, LNCS 443, Springer-Verlag, pp.322-335.
[5]F. Balarin. Approximate Reachability Analysis of Timed Automata. IEEE RTSS, 1996.
[6]J.R. Burch, E.M. Clarke, K.L. McMillan, D.L.Dill, L.J. Hwang. Symbolic Model Checking: 10^{20} States and Beyond.IEEE LICS, 1990.
[7]G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, Wang Yi.
Efficient Timed Reachability Analysis Using Clock Difference Diagrams. CAV''99, July, Trento, Italy, LNCS 1633, Springer-Verlag.
[8]J. V. Benthem, A. T. Meulen. Handbook of Logic and Language. North-Hooland, 1997.
[9]R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.
[10]C. Begin. Implementing the Microsoft .NET Pet Shop using Java. 2002 http://ibatis.apache.org/
[11]C. Begin. iBATIS Data Access Objects Developer Guide. 2004 http://ibatis.apache.org/
[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]D.L. Dill. Timing Assumptions and Verification of Finite-state Concurrent Systems. CAV''89, LNCS 407, Springer-Verlag.
[14]E.A. Emerson, C.-L. Lei. Modalities for Model Checking: Branching Time Logic Strikes Back, Science of Computer Programming 8 (1987), pp.275-306, Elsevier Science Publishers B.V. (North-Holland).
[15]E. A. Emerson. Uniform Inevitability is Tree Automaton Ineffable. Information Processing Letters 24(2), Jan 1987, pp.77-79.
[16]J.B. Fourier. (reported in:) Analyse des travaux de l''Acad''{e}mie Royale des Sciences pendant l''ann''{e}e 1824, Partie Math''{e}matique, 1827.
[17]G. Hamilton. Sun Microsystems JavaBeans. 1997 http://java.sun.com/beans.
[18]T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine.
Symbolic Model Checking for Real-Time Systems. IEEE LICS 1992.
[19]C.A.R. Hoare. Communicating Sequential Processes, Prentice Hall, 1985.
[20]B.W. Kernighan, D.M. Ritchie. The C Programming Language, 2ed. Prentice-Hall 1988.
[21]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.
[22]K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang. Efficient Verification of Real-Time Systems: Compact Data-Structure and State-Space Reduction. IEEE RTSS, 1998.
[23]J. Moller, J. Lichtenberg, H.R. Andersen, H. Hulgaard.
Difference Decision Diagrams. In proceedings of Annual Conference of the European Association for Computer Science Logic (CSL), Sept. 1999, Madreid, Spain.
[24]A. W. Mazurkiewicz, E. Ochmanski, W. Penczek. Concurrent Systems and Inevitability. TCS 64(3): 281-304,1989.
[25]G. N. Naumovich, L. A. Clarke, L. J. Osterweil. Verification of Communication Protocols using Data Flow Analysis. Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, pp. 93-105, 1996.
[26]P. Pettersson, K.G. Larsen. UPPAAL2k. Bulletin of the European Associatoin for Theoretical Computer Science, vol. 70, pp.40-44, 2000.
[27]H.T. Odum, E.C. Odum. Modeling for All Scales: an Introduction to System Simulation. Academic Press, 2000.
[28]C.-J. H. Seger, R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories.
Formal Methods in System Designs, Vol. 6, No. 2, pp. 147-189, Mar. 1995.
[29]F. Somemzi. CUDD: CU Decision Diagram Package,
ftp://vlsi.colorado.edu/pub, 1998.
[30]F. Wang. Scalable Compositional Reachability Analysis of Real-Time Concurrent Systems, 2nd IEEE RTAS, Boston, June 1996.
[31]F. Wang. Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS''2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag.
[32]F. Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. FORTE''2001, Kluwer; August 2001, Cheju Island, Korea.
[33]F. Wang. Tutorial II: Verification of Real-Time Systems with BDD-like Data-Structures, ATVA 2003, December 2003, Taipei, Taiwan.
[34]F. Wang. Model-Checking Distributed Real-Time Systems with States, Events, and Multiple Fairness Assumptions. 10th AMAST, % Stirling, UK, July 2004, LNCS 3116, Springer-Verlag.
[35]F. Wang. Efficient Verification of Timed Automata with BDD-like Data-Structures, STTT (Jouranl of Software Tools for Technology Transfer), Vol. 6, Nr. 1, June 2004, Springer-Verlag; Special issue for VMCAI''2003, LNCS 2575, Springer-Verlag.
[36]F. Wang. Formal Verification of Timed Systems - A Survey and Perspective. Proceedings of the IEEE, Vol. 92, Nr. 8, August 2004, pp.1283-1307, IEEE.
[37]F. Wang. Tutorial: Symbolic Techniques for the verification of real-time and embedded systems with BDD-like datastructures, 24th IFIP WG 6.1 FORTE, September 27-30, 2004, Madrid, Spain.
[38]F. Wang. Symbolic Parametric Analysis of Linear Hybrid Systems with BDD-like Data-Structures. IEEE Transactions on Software Engineering, January 2005 (Vol. 31, No. 1), p.38-51. A preliminary version of the paper also appears in proceedings of CAV 2004, LNCS 3114, Springer-Verlag.
[39]F. Wang, P.-A. Hsiung. Efficient and User-Friendly Verification. IEEE Transactions on Computers 51(1), Jan. 2002, pp.61-84.
[40]F. Wang, G.-D. Huang, F. Yu. TCTL Inevitability Analysis of Dense-Time Systems, in proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA), LNCS 2759, Springer-Verlag, July 2003, Santa Barbara, CA, USA.
[41]F. Wang, G.-D. Hwang, F. Yu. Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems. FORTE 2003, Sept.-Oct. 2003, Berlin, Germany; LNCS 2767, Springer-Verlag.
[42]F. Wang, C.-T. Lo. Procedure-Level Verification of Real-Time Concurrent Sytems, the Journal of Real-Time Systems, vol. 16, Nr. 1, Jan. 1999, pp.81-114, Kluwer Academic Publishers.
[43]F. Wang, A.K. Mok. A Verifier for Distributed Real-Time Systems with Bounded Integer Variables. COMPASS''93, Maryland, June 1993.
[44]F. Wang, A. Mok, E.A. Emerson. Symbolic Model-Checking for Distributed Real-Time Systems. In proceedings of 1st FME, April 1993, Denmark; LNCS 670, Springer-Verlag.
[45]F. Wang, K. Schmidt, F. Yu, G.-D. Huang, B.-Y. Wang. BDD-based Safety-Analysis of Concurrent Software with Pointer Data Structures using Graph Automorphism Symmetry reduction. IEEE Transactions on Software Engineering, Vol. 30, Nr. 6, June 2004, ISSN 0098-5589, pp.403-417, IEEE.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔