請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/24365完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 王凡(Farn Wang) | |
| dc.contributor.author | Kai-Rong Chang | en |
| dc.contributor.author | 張凱榮 | zh_TW |
| dc.date.accessioned | 2021-06-08T05:23:22Z | - |
| dc.date.copyright | 2005-07-28 | |
| dc.date.issued | 2005 | |
| dc.date.submitted | 2005-07-25 | |
| dc.identifier.citation | [1] E. Mendelson, Intrduction to Mathematical Logic, D. Van Nostrand Company, Inc., Princeton, N.J., 1964
[2] E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic. Lecture Notes in Computer Science, Logic of Programs. Heidelberg, Germany: Springer-Verlag, 1981, vol. 131, pp. 52V71. [3] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP’ 1990, LNCS 443, Springer-Verlag, pp.322-335. [4] R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems. IEEE LICS, 1990. [5] 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). [6] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP’ 1990, LNCS 443, Springer-Verlag, pp.322-335. [7] 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. [8] F. Wang. E cient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag. [9] F. Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. FORTE’2001, Kluwer; August 2001, Cheju Island, Korea. [10] F. Wang. E cient Verification of Timed Automata with BDD-like Data-Structures. special issue of STTT (Software Tools for Technology Transfer), Springer-Verlag for VMCAI’2003 [11] F. Wang. E cient 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. [12] F. Wang. Symbolic Parametric Analysis of Linear Hybrid Systems with BDDlike 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. [13] 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. [14] J.-M. Wang. Formal modeling and verification of a Third Generation Mobile Communication Protocol. Master thesis in Department of Electrical Engineering, Nation Taiwan University, 2004. [15] L.-D.Wang. The Implementation of Automated Translator from Programming Language to Timed Automata. Master thesis in Department of Electrical Engineering, Nation Taiwan University, 2004. [16] 3GPP TS 25.301: ”Radio Interface Protocol Architecture”. [17] 3GPP TS 25.322: ”Radio Link Control (RLC) protocol specification”. [18] T. Mason, D. Brown, LEX and YACC, O’Reilly, 1990. [19] http://www.gnu.org/ [20] A. Finkel. Decidability of the termination problem for completely specified protocols. In Distributed Computing, 7(3), pp129-135, 1994 [21] Parosh Aziz Abdulla and Bengt Jonsson. Verifying Programs with Unreliable Channels. Journal of Information and Computation. 127(2):91-101, 1996. [22] A. Annichini, A. Bouajjani, and M.Sighireanu. TreX: A Tool for Reachability Analysis of Complex Systems. To appear in Proceedings of CAV 2001. (C)Springer-Verlag. [23] P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proceedings of 3rd Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217 of LNCS, page 416-432. Springer Verlag, 1997 [24] Open Verification Library http://www.accellera.org/ [25] E. Clarke and J.Wing. Formal Methods: State of the Art and Future Directions, CMU Computer Science Technical Report CMU-CS-96-178, August 1996. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/24365 | - |
| dc.description.abstract | 隨著軟硬體設計複雜度快速地增加，傳統的驗證技術已不敷使用。許多人把焦點進而轉向了正規驗證，希望能利用正規驗證的技術來達成更有效率及可靠的驗證。正規驗證的技術可以幫助我們輕易且自動化地找出潛藏的設計錯誤。然而正規驗證的技術並不是完全毫無缺點，與其他驗證技術相比，其中一項較為弱勢的地方在於描述待驗證系統的正規語言。正規語言為了配合數學模型，其本身的語法通常較為精簡，換句話說在描述較複雜的系統時，也相對的較為困難。因此，我們欲開發一個正規模型函式庫，來改善正規語言的不足。利用自動轉譯成原有語法的方式，使得我們可以在不改變原有驗證系統核心的情況下，輕易地使用較高階的語法來描述待驗證系統，以縮短建立正規化模型的時間。目前正規模型函式庫包含了channel, array, memory allocation, procedure call及timer。 | zh_TW |
| dc.description.abstract | With the rapidly increasing design complexity, traditional techniques for validness such as simulation and testing are not su cient. The formal methods for verification have become the limelight. The corner cases might be detected easily and automatically by these formal techniques. In spite of the fact that formal verification is such powerful, the formal methods have still been limited to some issues. One subject is that the formal languages are too simple to describe the design systems. Hence we construct a model library which contains channel, array, memory allocation, procedure call, and timer currently to improve the work of building model. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-08T05:23:22Z (GMT). No. of bitstreams: 1 ntu-94-R92921123-1.pdf: 411808 bytes, checksum: c40892c0f33ec20fd30ce827519e4d07 (MD5) Previous issue date: 2005 | en |
| dc.description.tableofcontents | Contents i
List of Figures iii List of Tables 1 1 Introduction 2 1.1 Motivation 3 1.2 Thesis Organization 3 2 Verification System: RED 5 2.1 Communicating Timed Automata 5 2.2 Input File Structure of RED 6 3 Syntax and Translation Mechanism of Models 10 3.1 Channel 11 3.2 Array 13 3.3 Memory Allocation 15 3.4 Procedure Call 17 3.5 Timer 18 4 Implementation 22 4.1 Framework22 4.2 Data Structure 25 5 Experiment 27 6 Conclusions and FutureWork 30 7 RelatedWork 32 A The Overview of RLC protocol 34 A.1 Modes of RLC 34 A.1.1 TM Mode 34 A.1.2 UM Mode 35 A.1.3 AM Mode 37 A.2 Protocol States of RLC 40 A.2.1 State Model for TM Entities 40 A.2.2 State Model for UM Entities 40 A.2.3 State Model for AM Entities 42 Bibliography 46 | |
| dc.language.iso | en | |
| dc.subject | 語法 | zh_TW |
| dc.subject | 正規方法 | zh_TW |
| dc.subject | 正規驗證 | zh_TW |
| dc.subject | 正規化模型 | zh_TW |
| dc.subject | 函式庫 | zh_TW |
| dc.subject | syntax | en |
| dc.subject | formal methods | en |
| dc.subject | formal verification | en |
| dc.subject | formal model | en |
| dc.subject | library | en |
| dc.title | 嵌入式系統在正規化模型語法上的增進與提升 | zh_TW |
| dc.title | Syntactical Enhancement in the Formal Models of Embedded Systems | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 93-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 雷欽隆(Chin-Laung Lei),王勝德(Sheng-De Wang),李允中(Jonathan Lee),張嘉祥(Chia-Hsiang Chang) | |
| dc.subject.keyword | 正規方法,正規驗證,正規化模型,函式庫,語法, | zh_TW |
| dc.subject.keyword | formal methods,formal verification,formal model,library,syntax, | en |
| dc.relation.page | 47 | |
| dc.rights.note | 未授權 | |
| dc.date.accepted | 2005-07-25 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 電機工程學研究所 | zh_TW |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-94-1.pdf 未授權公開取用 | 402.16 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。