Automatic Construction of Formal Models for Embedded Systems
| Autor: | Rong-Shiung Wu, 吳榮軒 |
|---|---|
| Rok vydání: | 2005 |
| Druh dokumentu: | 學位論文 ; thesis |
| Popis: | 93 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. |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|