VISUAL FORMALISM, STATECHARTS, AND STATEMATE Finite-state machines (FSMs) have been used extensively in the specification and analysis of many computer-based as well as non-computer-based systems, ranging from electronic circuits to econometric models. They can model in detail the behavior of a system, and several algorithms exist to perform the analysis. Unfortunately, classical state machines such as those employed in the standard, explicit-state CTL model-checking approach [Clarke, Emerson, and Sistla, 1986] lack support for modularity and suffer from exponential-state explosion. . | Real-Time Systems Scheduling Analysis and Verification. Albert M. K. Cheng Copyright 2002 John Wiley Sons Inc. ISBN 0-471-18406-3 CHAPTER 5 VISUAL FORMALISM STATECHARTS AND STATEMATE Finite-state machines FSMs have been used extensively in the specification and analysis of many computer-based as well as non-computer-based systems ranging from electronic circuits to econometric models. They can model in detail the behavior of a system and several algorithms exist to perform the analysis. Unfortunately classical state machines such as those employed in the standard explicit-state CTL model-checking approach Clarke Emerson and Sistla 1986 lack support for modularity and suffer from exponential-state explosion. The first problem often arises when FSMs are used to model complex systems that contain similar subsystems. The second problem is evident in systems in which the addition of a few variables or components can substantially increase the number of states and transitions and hence the size of the FSM. Furthermore the inability to specify absolute time and time intervals limits the usability of classical FSMs for the specification of real-time systems. To tackle the first two problems we can introduce modular and hierarchical features to classical FSMs. Harel et al. 1987 developed a visual formalism called Statecharts to solve these two problems as well as the problem of specifying reactive systems. Reactive systems are complex control-driven mechanisms that interact with discrete occurrences in the environment in which they are embedded. They include real-time computer systems communication devices control plants VLSI circuits and airplane avionics. The reactive behavior of these systems cannot be captured by specifying the corresponding outputs resulting from every possible set of inputs. Instead this behavior has to be described by specifying the relationship of inputs outputs and system state over time under a set of system- and environment-dependent timing and .
