Model checking of hierarchical state machines

Details Model checking of hierarchical state machines Model checking of hierarchical state machines

1998-06-18

2001-11-27

Teska, Kevin J. (Department: 2123)

Data processing: structural design, modeling, simulation, and em

Simulating electronic device or electrical system

Event-driven

C703S022000, C714S039000, C716S030000

Reexamination Certificate

active

06324496

ABSTRACT:

BACKGROUND OF THE INVENTION
1. Field of the Invention
The present invention relates to finite state machines, and, in particular, to model checking of hierarchical state machines.
2. Description of the Related Art
Finite state machines (FSMs) are widely used in the modeling of systems in various areas. Descriptions using FSMs are useful to represent the flow of control (as opposed to data manipulation) and are amenable to formal analysis such as model checking. In the simplest setting, an FSM consists of a labeled graph whose vertices correspond to system states and whose edges correspond to system transitions.
In practice, to describe complex systems using FSMs, extensions from this basic FSM definition are useful, including the following three orthogonal extensions: (1) communicating FSMs, in which annotations are added so that transitions within different FSMs corresponding to different components can be synchronized; (2) extended FSMs, in which variables, such as counters and buffers, together with guarded assignments on transitions, are added to allow succinct description; and (3) hierarchical or nested FSMs, in which vertices of an FSM can be ordinary states or superstates that are themselves FSMs. While the impact of adding the first two features to the complexity of analysis problems has been well understood, this has not been the case with regard to the impact of the third feature.
The ability to nest FSMs is common in many specification formalisms and methods. It is a central component of various object-oriented software development methodologies that have been developed in recent years. This capability is commonly available also in commercial computer-aided software engineering tools that are coming out.
The nesting capability is useful also in formalisms and tools for the requirements and testing phases of the software development cycle. On the requirements side, it is used to specify scenarios (or use cases) in a structured manner. For instance, the International Telecommunication Union (ITU) standard Z.120 for message sequence charts formalizes scenarios of distributed systems in terms of hierarchical graphs built from basic message sequence charts. On the testing side, FSMs are used often to model systems for the purpose of test generation, and again the nesting capability is useful to model large systems. This is useful for systems with informal and incomplete requirements and design documentation, as is often the case, and especially for software that was developed and evolved over a long period of time, when the test models are updated for continued regression testing as the system evolves.
An example of a hierarchical FSM is a digital clock. The top-level state machine for a digital clock may consist of a cycle through 24 superstates, with each superstate corresponding to a different hour of the day. Each such state, in turn, is a hierarchical state machine consisting of a cycle through 60 superstates counting minutes, each of which, in turn, is an (ordinary) state machine consisting of a cycle counting 60 seconds.
Hierarchical state machines have two descriptive advantages over ordinary FSMs. First, superstates offer a convenient structuring mechanism that allows a system to be specified in a stepwise refinement manner, where the system can be viewed at different levels of granularity. Such structuring is particularly useful for specifying large FSMs via a graphical interface. Second, by allowing sharing of component FSMs, components need to be specified only once and then reused in different contexts, leading to modularity and succinct system representations. For instance, the 24 superstates of the top-level FSM for the digital clock can be mapped to the same hierarchical FSM corresponding to an hour, and the 60 superstates corresponding to the minutes of each hour can be mapped to the same ordinary FSM corresponding to a second.
Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. As such, model checking is particularly useful in automated debugging of complex reactive systems such as embedded controllers and network protocols. In model checking, a high-level description of a system is compared against a correctness requirement to discover inconsistences.
The straightforward approach to applying model checking to a hierarchical state machine is to flatten it (i.e., recursively substitute each superstate with its associated FSM) and then apply a model checking tool to the resulting ordinary FSM. Such flattening, however, can cause a large blow-up in the size of the state machine, particularly when there is a lot of sharing of component FSMs. For instance, the hierarchical description of the digital clock has 24+60+60=144 vertices, while the equivalent flattened FSM has 24*60*60=86,400 vertices. Thus, if the hierarchical state machine is first flattened and then subjected to a conventional model checking algorithm, the worst-case complexity would be exponential in the original description of the structure. The amount of computer memory needed to represent such flattened FSMs can be prohibitively large.
SUMMARY OF THE INVENTION
According to the present invention, model checking is applied to hierarchical state machines without first flattening the state machine.
The model checking may include a reachability analysis in which reachability of one or more target states is determined while maintaining (1) a first set of information to keep track of states that have been visited during the reachability analysis, and (2) a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine.
In addition or alternatively, the model checking may include a cycle-detection analysis in which reachability of one or more target states existing in a closed processing path is determined while maintaining (1) a first set of information to keep track of states that have been visited during a first phase of the cycle-detection analysis in which reachability of at least one of the one or more target states is determined, (2) a second set of information to keep track of one or more exit nodes for each state in the hierarchical state machine that is a superstate corresponding to a finite state machine, and (3) a third set of information to keep track of states that have been visited during a second phase of the cycle-detection analysis in which it is determined whether a reachable target state is part of a closed processing path.
In addition or alternatively, the model checking may include a linear-time requirements analysis in which a formula is translated into an automaton. A product construction is defined between the automaton and a hierarchical machine that yields a new hierarchical machine that is then analyzed using the cycle-detection algorithm.
In addition or alternatively, the model checking may include a branching-time requirements analysis in which states in the hierarchical state machine are identified that satisfy one or more temporal logic requirements, wherein, for each temporal logic requirement, multiple versions are generated of the FSM corresponding to each state in the hierarchical state machine that is a superstate to represent different possible temporal logic conditions of the FSM and an appropriate FSM version is selected for the context of each occurrence of the superstate in the hierarchical state machine.


REFERENCES:
patent: 4930072 (1990-05-01), Agrawal et al.
patent: 5163016 (1992-11-01), Har'El et al.
patent: 5291427 (1994-03-01), Loyer et al.
patent: 5463563 (1995-10-01), Bair et al.
patent: 5513122 (1996-04-01), Cheng et al.
patent: 5606698 (1997-02-01), Powell
patent: 5680332 (1997-10-01), Raimi et al.
patent: 5752241 (1998-05-01), Cohen
patent: 5764951 (1998-06-01), Ly et al.
patent: 5937195 (1999-08-01), Ju et al.
patent: 5995739 (1999-11-01), Rotbart
patent: 5999717 (1999-12-01), Kaufmann et al.
patent: 6009250 (1999-12-01), Ho et al.
patent: 6175946

Affiliated with

Also associated with

Rating

Model checking of hierarchical state machines does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Model checking of hierarchical state machines, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model checking of hierarchical state machines will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2575194