嵌入式系統正規模型之自動化建立

Automatic Construction of Formal Models for Embedded Systems

吳榮軒(Rong-Shiung Wu)

指導教授 ： 王凡

國立臺灣大學/電機資訊學院/電機工程學研究所/碩士(2005年)

https://doi.org/10.6342/NTU.2005.00324

摘要

系統描述語言是一種正規化的標準語言，用來描述系統的規格。它更
是專門被設計來描述具有事件觸發性、即時系統性及互動性的案例
上，這些案例上的系統都是同時運作並且藉由訊息的傳遞來溝通。系
統描述語言描述的是一個系統的行為表現。為了要用正規方法來驗證
這樣的一個描述系統，我們必須先建立正規化的模型。而在這篇論文
裡面，我們為一個用系統描述語言描述的嵌入式系統建立時間自動機
的模型。我們也設計並且實作了一些轉換的方法來自動轉換一個用系
統描述語言描述的系統成時間自動機的模型，因此模型的建立與驗證
可望以有效率、秩序及沒有錯誤的方式進行。

關鍵字

系統描述語言 ； 正規模型 ； 時間自動機

並列摘要

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.

並列關鍵字

SDL ； formal model ； timed automata

參考文獻

guage Design and Implementation, 1998.

Nr. 1, June 2004, Springer-Verlag; Special issue for VMCAI'2003, LNCS 2575,

[1] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP' 1990, LNCS

[2] R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems. IEEE

[3] A. Aalto, N. Husberg, K. Varpaaniemi. Automatic formal model generation and