UML-based Verification of Semantic Finite State Machine

• Main Authors: Yun-Hau Yang, 楊雲豪
• Other Authors: Chang-Jen Tang
• Format: Others
• Language: zh-TW
• Published: 2004
• Online Access: http://ndltd.ncl.edu.tw/handle/30646345601178252034

碩士 === 大同大學 === 電機工程研究所 === 92 === Unified Modeling Language (UML) provides a simple and easy tool for the specification and requirement of systems. It is rapidly becoming an industrial standard for object-oriented modeling and analysis. According to its flexibility, this thesis adopts UML to build the model of finite state machine (FSM) structure in HDL. In addition, the model checker is SPIN that results from codes in description of PROMELA. Semantic Finite State Machine (SFSM) presents complete definitions to explain circuits structured by hardware description language (HDL) in the abstract level. HDL depicts digital circuit in several methods, but structural behavior description is especially for sequential circuit. SFSM provides definitions for behavior description in HDL, and UML is used to build a model in abstract level and visualize the model to easily understand. In addition to verification with binary deriving such as Karnaugh graph, binary decision diagram, this thesis proposes an abstract concept to portray the design that is based on states. Finally, the experimental result is produced after model checking with SPIN and model building with UML.