請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/38481完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 王凡(Farn Wang) | |
| dc.contributor.author | Rong-Shiung Wu | en |
| dc.contributor.author | 吳榮軒 | zh_TW |
| dc.date.accessioned | 2021-06-13T16:34:52Z | - |
| dc.date.available | 2005-07-26 | |
| dc.date.copyright | 2005-07-26 | |
| dc.date.issued | 2005 | |
| dc.date.submitted | 2005-07-08 | |
| dc.identifier.citation | [1] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP' 1990, LNCS
443, Springer-Verlag, pp.322-335. [2] R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems. IEEE LICS, 1990. [3] A. Aalto, N. Husberg, K. Varpaaniemi. Automatic formal model generation and analysis of SDL. In SDL 2003: System Design, 11th International SDL Forum, Stuttgart, Germany, July 1V4, 2003. [4] M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, J. Sifakis. IF: An Intermediate Representation for SDL and its Applications. Proceedings of SDL-Forum'99 (Montreal, Canada) June 1999. [5] F. Belina, D. Hogrefe and A. Sarma. SDL with APPLICATIONS from PROTO- COL speci‾cation. Prentice Hall 1991, ISBN 0-13-785890-6. [6] C. Colby, P. Godefroid, L.J. Jagadeesan. Automatically Closing Open Reactive Programs. in Proceedings of ACM SIGPLAN Conference on Programming Lan- guage Design and Implementation, 1998. [7] 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). [8] E.M. Clarke, O. Grumberg, D.A. Peled Model Checking. MIT Press, 2000, ISBN 0-262-03270-8. [9] A. Hessel. Timing analysis of an SDL subset in Uppaal. Master thesis in Institution of Information Technology Department of Computer Systems, Uppsala University, 2002. [10] C.A.R. Hoare. Communicating Sequential Processes, Prentice Hall, 1985. [11] IF project at http://www-verimag.imag.fr/DIST SYS/IF/index.html [12] ITU-T Recommendation Z.100, Speci‾cation and Description Language (SDL), Geneva, 1992. [13] F. Regensburger, A. Barnard. Formal Veri‾cation of SDL Systems at the Siemens Mobile Phone Department. in Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems. 1998. [14] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP' 1990, LNCS 443, Springer-Verlag, pp.322-335. [15] S. Redl, M.W. Oliphant, M.K. Weber. An Introduction to GSM. Artech House, Inc. 1995 ISBN:0890067856. [16] SDL Forum at http://www.sdl-forum.org/SDL/ [17] L.J. Steggles, P. Kosiuczenko. A Formal Model for SDL Speci‾cations Based on Timed Rewriting Logic. Automated Software Engineering, v.7 n.1, p.61-90, March 2000. [18] N. Sidorova, M. Ste®en. Embedding Chaos. In Proceedings of 8th International Static Analysis Symposium, SAS 2001, Paris, France, 2001. [19] Telelogic Tau SDL suite. http://www.telelogic.com/ [20] H. Tuominen. Embedded a Dialect of SDL in PROMELA. in proceedings of 6th International SPIN Workshop, 1999. [21] F. Wang. E±cient Data-Structure for Fully Symbolic Veri‾cation of Real- Time Software Systems. TACAS'2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag. [22] F. Wang. Symbolic Veri‾cation of Complex Real-Time Systems with Clock- Restriction Diagram. FORTE'2001, Kluwer; August 2001, Cheju Island, Korea. [23] F. Wang. E±cient Veri‾cation of Timed Automata with BDD-like Data- Structures. special issue of STTT (Software Tools for Technology Transfer), Springer-Verlag for VMCAI'2003 [24] F. Wang. E±cient Veri‾cation 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. [25] 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. [26] F. Wang, G.-D. Huang, F. Yu. TCTL Inevitability Analysis of Dense-Time Sys- tems, in proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA), LNCS 2759, Springer-Verlag, July 2003, Santa Barbara, CA, USA. [27] S. Yovine. Kronos: A Veri‾cation Tool for Real-Time Systems. International Jour- nal of Software Tools for Technology Transfer, Vol. 1, Nr. 1/2, October 1997. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/38481 | - |
| dc.description.abstract | 系統描述語言是一種正規化的標準語言，用來描述系統的規格。它更
是專門被設計來描述具有事件觸發性、即時系統性及互動性的案例 上，這些案例上的系統都是同時運作並且藉由訊息的傳遞來溝通。系 統描述語言描述的是一個系統的行為表現。為了要用正規方法來驗證 這樣的一個描述系統，我們必須先建立正規化的模型。而在這篇論文 裡面，我們為一個用系統描述語言描述的嵌入式系統建立時間自動機 的模型。我們也設計並且實作了一些轉換的方法來自動轉換一個用系 統描述語言描述的系統成時間自動機的模型，因此模型的建立與驗證 可望以有效率、秩序及沒有錯誤的方式進行。 | zh_TW |
| dc.description.abstract | SDL is a formal standardized notation for the speci‾cation of systems. It is intended to describe event-driven, real-time and interactive applications involving many
concurrent activities that communicate with discrete signals. It describes the behavior aspect of systems. In order to verify an SDL speci‾cation by formal methods, the for- mal models are build. In this thesis, the timed automata is used to model an embedded system described in SDL. We also design and implement the translation mechanisms to automatically translate the supported SDL syntax into the timed automata. Therefore the modelling and veri‾cation of an SDL speci‾cation can be e±cient, ordered and error-free. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-13T16:34:52Z (GMT). No. of bitstreams: 1 ntu-94-R92921076-1.pdf: 591506 bytes, checksum: 4ef0c2bd0c22b8a8c049dbd6c65f636e (MD5) Previous issue date: 2005 | en |
| dc.description.tableofcontents | Contents i
List of Figures iv Acknowledgements vi 1 Introduction 1 2 Speci‾cation Description Language 4 2.1 System structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Behavior overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Abstract data type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.1 Simple prede‾ned sorts in SDL . . . . . . . . . . . . . . . . . . 9 2.3.2 User-de‾ned sorts in SDL . . . . . . . . . . . . . . . . . . . . . 9 2.3.3 Variable declarations . . . . . . . . . . . . . . . . . . . . . . . . 11 2.4 Representation forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.5 Process declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.5.1 Triggering Condition . . . . . . . . . . . . . . . . . . . . . . . . 13 2.5.2 Transition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.6 Communicating SDL processes . . . . . . . . . . . . . . . . . . . . . . . 19 2.6.1 Using the save construct in SDL . . . . . . . . . . . . . . . . . . 20 2.6.2 Time and timers . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.6.3 Signalroutes and channels . . . . . . . . . . . . . . . . . . . . . 23 3 Communicating Timed Automata 24 3.1 De‾nition of CTA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.2 RED input ‾le structure . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.3 Modelling CSMA/CD protocol . . . . . . . . . . . . . . . . . . . . . . . 31 3.4 Model library in RED . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.5 Timed Event CTL with Fairness assumptions . . . . . . . . . . . . . . 34 4 Translation Mechanism 36 4.1 SDL sort conversion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.1.1 Prede‾ned sorts . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.1.2 User-de‾ned sorts . . . . . . . . . . . . . . . . . . . . . . . . . . 39 4.2 Queue declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.3 Timer declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 4.4 SDL process behavior translation . . . . . . . . . . . . . . . . . . . . . 44 4.4.1 Triggering Condition . . . . . . . . . . . . . . . . . . . . . . . . 44 4.4.2 Action statements . . . . . . . . . . . . . . . . . . . . . . . . . . 45 4.4.3 Termination statements . . . . . . . . . . . . . . . . . . . . . . 50 5 Examples 52 5.1 Sender-receiver scheme . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 5.2 Simpli‾ed GSM network . . . . . . . . . . . . . . . . . . . . . . . . . . 55 6 Related Works 60 7 Conclusions and Future Works 62 A Syntax Summary of SDLred 64 A.1 Backus-Naur Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 A.2 Lexical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 A.3 Syntactical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 B CSMA/CD with two sender processes 73 C The SDL description of the sender-receiver example 75 D The translated result of the sender-receiver example 78 Bibliography 84 | |
| dc.language.iso | en | |
| dc.subject | 系統描述語言 | zh_TW |
| dc.subject | 正規模型 | zh_TW |
| dc.subject | 時間自動機 | zh_TW |
| dc.subject | formal model | en |
| dc.subject | SDL | en |
| dc.subject | timed automata | en |
| dc.title | 嵌入式系統正規模型之自動化建立 | zh_TW |
| dc.title | Automatic Construction of Formal Models for Embedded Systems | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 93-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 王柏堯(Bow-Yaw Wang),張嘉祥(Chia-Hsiang Chang),雷欽隆(Chin-Laung Lei),戴顯權(Shen-Chuan Tai) | |
| dc.subject.keyword | 系統描述語言,正規模型,時間自動機, | zh_TW |
| dc.subject.keyword | SDL,formal model,timed automata, | en |
| dc.relation.page | 86 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2005-07-08 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-94-1.pdf 未授權公開取用 | 577.64 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。