.png){kind=icon}
.png){kind=icon}
Return
Simulation-verification: Biting at the state explosion problem
.png){kind=icon}
PRE
AI
DOI：10.1109/32.935853.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Simulation and verification are the two conventional techniques for the analysis of specifications of real-time systems. While simulation is relatively inexpensive in terms of execution time, it only validates the behavior of a system for one particular computation path. On the other hand, verification provides guarantees over the entire set of computation paths of a system. but is, in general. very expensive due to the state-space explosion problem. In this paper, we introduce a new technique: Simulation-verification combines the best of both worlds by synthesizing an intermediate analysis method. This method uses simulation to limit the generation of a computation graph to that set of computations consistent with the simulation. This limited computation graph, called a simulation-verification graph, can be one or more orders of magnitude smaller than the full computation graph. A tool, XSVT, is described which implements simulation-verification graphs. Three paradigms for using the new technique are proposed. The paper illustrates the application of the proposed technique via an example of a robot controller for a manufacturing assembly line.
Keywords:
real-time systems
formal methods
specification
verification
timing constraints
Modechart
requirements analysis
simulation
Journal
IF:
5.6
Papers:
2.8K
Citations:
1.1W
Organization
No organization information available