Back to results
US 6,324,496 B1Granted
Model checking of hierarchical state machines
AssigneeLucent Technologies Inc.
InventorsRajeev Alur, Mihalis Yannakakis
Life of this patent
Estimating the term…
Loading patent…
Loading patent…
AssigneeLucent Technologies Inc.
InventorsRajeev Alur, Mihalis Yannakakis
Estimating the term…
Model checking is applied to a hierarchical state machine (i.e., a state machine having at least one state (i.e., a superstate) that is itself a state machine) without first flattening the hierarchical state machine. In one embodiment, the model checking involves one or more or reachability, cycle-detection, linear-time requirements, and branching-time requirements analyses. For reachability analysis, in addition to keeping track of whether states have been visited, the algorithm also keeps track of the exit nodes for each superstate. Cycle-detection analysis has two phases: a primary phase in which target states are identified and a secondary phase in which it is determined whether identified target states are part of closed processing paths or loops. For cycle-detection analysis, the algorithm keeps track of (1) whether states have been visited during the primary phase, (2) the exit nodes for each superstate, and (3) whether states have been visited during the secondary phase. For linear-time requirements analysis, a formula is translated into an automaton, and 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. For branching-time requirements analysis, a list of subformulas is generated for an original temporal logic formula, where the subformulas are arranged in order of increasing size. An appropriate subroutine is then implemented for each subformula in the list based on the syntax of the subformula. For certain syntaxes, multiple versions are generated of the finite state machine corresponding to each superstate to represent different possible temporal logic conditions, and an appropriate version is selected for the context of each occurrence of the superstate in the hierarchical state machine. After processing the entire list of subformulas, it is determined whether the entry node of the hierarchical state machine satisfies the original temporal logic formula.
A computer-implemented method for testing a hierarchical state machine that models flow of control within a real system, comprising the steps of:
A machine-readable medium having stored thereon a plurality of instructions, the plurality of instructions including instructions that, when executed by a computer, cause the computer to perform a method for testing a hierarchical state machine that models flow of control within a real system, comprising the steps of:
A computer-implemented method for testing a hierarchical state machine that models flow of control within a real system, wherein the real system is a circuit or a computer program and model checking is applied to the hierarchical state machine without first flattening the hierarchical state machine, wherein the hierarchical state machine is a finite state machine comprising a plurality of states, wherein at least two of the states are multiple instances of a single state machine and the model checking comprises comparison of the hierarchical state machine against at least one correctness requirement to determine whether the hierarchical state machine satisfies the at least one correctness requirement, wherein, during the model checking, each state machine having multiple instances in the hierarchical state machine is analyzed fewer times than its number of instances in the hierarchical state machine using cyclic temporal logic relation.
Dependencies are inferred from the claim text.