王凡臺灣大學：電機工程學研究所吳榮軒Wu, Rong-ShiungRong-ShiungWu2007-11-262018-07-062007-11-262018-07-062005http://ntur.lib.ntu.edu.tw//handle/246246/53265系統描述語言是一種正規化的標準語言，用來描述系統的規格。它更 是專門被設計來描述具有事件觸發性、即時系統性及互動性的案例 上，這些案例上的系統都是同時運作並且藉由訊息的傳遞來溝通。系 統描述語言描述的是一個系統的行為表現。為了要用正規方法來驗證 這樣的一個描述系統，我們必須先建立正規化的模型。而在這篇論文 裡面，我們為一個用系統描述語言描述的嵌入式系統建立時間自動機 的模型。我們也設計並且實作了一些轉換的方法來自動轉換一個用系 統描述語言描述的系統成時間自動機的模型，因此模型的建立與驗證 可望以有效率、秩序及沒有錯誤的方式進行。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.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 84591506 bytesapplication/pdfen-US系統描述語言正規模型時間自動機SDLformal modeltimed automatathesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53265/1/ntu-94-R92921076-1.pdf