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

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.