Alur, Rajeev; Henzinger, Thomas AIST Austria ; Rajamani, Sriram K
In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially—and in some cases, fully—bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers. Specifically, we present the following contributions: - A temporal abstraction operator that aggregates transitions and hides intermediate steps. Mathematically, our abstraction operator is a function that maps a flat transition system into a two-level hierarchy where each atomic upper-level transition expands into an entire lower-level transition system. For example, an arithmetic operation may expand into a sequence of bit operations. - A BDD-based algorithm for the symbolic exploration of multi-level hierarchies of transition systems. The algorithm traverses a level-n transition by expanding the corresponding level-(n − 1) transition system on-the-fly. The level-n successors of a state are determined by computing a level-(n − 1) reach set, which is then immediately released from memory. In this fashion, we can exhaustively explore hierarchically structured state spaces whose flat counterparts cause memory overflows. - We experimentally demonstrate the efficiency of our method with three examples—a multiplier, a cache coherence protocol, and a multiprocessor system. In the first two examples, we obtain significant improvements in run times and peak BDD sizes over traditional state-space search. The third example cannot be model checked at all using conventional methods (without manual abstractions), but can be analyzed fully automatically using transition hierarchies.
This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Air Force Office of Scientific Research contract F49620-93-1-0056, by the Army Research Office MURI grant DAAH-04-96-1-0341, by the Advanced Research Projects Agency grant NAG2-892, and by the Semiconductor Research Corporation contract 95-DC-324.036.
330 - 344
TACAS: Tools and Algorithms for the Construction and Analysis of Systems
Alur R, Henzinger TA, Rajamani S. Symbolic exploration of transition hierarchies. In: Vol 1384. Springer; 1998:330-344. doi: 10.1007/BFb0054181
Alur, R., Henzinger, T. A., & Rajamani, S. (1998). Symbolic exploration of transition hierarchies (Vol. 1384, pp. 330–344). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer. https://doi.org/ 10.1007/BFb0054181
Alur, Rajeev, Thomas A Henzinger, and Sriram Rajamani. “Symbolic Exploration of Transition Hierarchies,” 1384:330–44. Springer, 1998. https://doi.org/ 10.1007/BFb0054181.
R. Alur, T. A. Henzinger, and S. Rajamani, “Symbolic exploration of transition hierarchies,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 1998, vol. 1384, pp. 330–344.
Alur R, Henzinger TA, Rajamani S. 1998. Symbolic exploration of transition hierarchies. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1384. 330–344.
Alur, Rajeev, et al. Symbolic Exploration of Transition Hierarchies. Vol. 1384, Springer, 1998, pp. 330–44, doi: 10.1007/BFb0054181.