Automatic Construction of Formal Models for Embedded Systems
Date Issued
2005
Date
2005
Author(s)
Wu, Rong-Shiung
DOI
en-US
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.
Subjects
系統描述語言
正規模型
時間自動機
SDL
formal model
timed automata
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-94-R92921076-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):c9abcaee147f3969f6604c8796434dc2