The modern systems engineering demands rapid implementation and quality. Graphical modeling and simulation provides a solution to verify the design goals proactively and to reduce the cost.In this paper, we present a graphical model based on the state machine. We set the design goals of a system via the graphical model, and we verify the design goals in the modeling process. We also give a description of the syntax and semantics of the state machine. We take the Extended Hierarchical Automaton (EHA) as the intermediate model to create the Labeled Transition System (LTS). This avoids the destruction of the structures. We derive the corresponding Büchi automaton. We study the LTL formulae on describing the characteristics of a system and we present a method of converting the LTL formulae to the Büchi automaton. By examing the product of these two automata, we are able to verify the properties of the modeled system. Because of the parallel and hierarchical nature of the state machine and the complexity in its semantics, state explosion exists in the process of model verification. We present a discussion on this issue in the paper. |