Abstract
A fundamental difficulty in automatic formal verification of finite-state systems is thestate explosion problem—even relatively simple systems can produce very large state spaces, causing great difficulties for methods that rely on explicit state enumeration. We address the problem by exploiting structuralsymmetries in the description of the system to be verified.
We make symmetries easy to detect by introducing a new data typescalarset, a finite and unordered set, to our description language. The operations on scalarsets are restricted so that states are guaranteed to have the same future behaviors, up to permutation of the elements of the scalarsets. Using the symmetries implied by scalarsets, a verifier can automatically generate a reduced state space, on the fly. We provide a proof of the soundness of the new symmetry-based verification algorithm based on a definition of the formal semantics of a simple description language with scalarsets.
The algorithm has been implemented and evaluated on several realistic high-level designs. Memory requirements were reduced by amounts ranging from 83% to over 99%, with speedups ranging from 65% to 98%.
Symmetry-based reduction leads to an alternative characterization ofdata independence: a protocol is data-independent if there is a scalarset type not used as an array index orfor loop index. In this case, symmetry-based reduction converts an infinite state space to a finite state space. Unlike other methods that exploit data independence in verification, this reduction occurs completely automatically.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
S. Aggarwal, R.P. Kurshan, and K. Sabnani, “A calculus for protocol specification and validation,”Protocol Specification, Testing, and Verification, Vol. 3, pp. 19–34, 1983.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic model checking: 1020 states and beyond,”Proc. 5th Ann. IEEE Symp. on Logic in Computer Science, pp. 428–439, 1990.
K.M. Chandy and J. Misra,Parallel Program Design—A Foundation, Addison-Wesley, 1988.
E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,”ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, 1986.
E.M. Clarke, T. Filkorn, and S. Jha, “Exploiting symmetry in temporal logic model checking,”5th International Conference on Computer-Aided Verification, pp. 450–462, June 1993.
O. Coudert, C. Berthet, and J.C. Madre, “Verification of synchronous sequential machines based on symbolic execution,”Automatic Verification Methods for Finite State Systems, pp. 365–373, 1989.
D.L. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang, “Protocol verification as a hardware design aid,”Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers and Processors, pp. 522–525, 1992.
C. Ebeling, “GeminiII: A second generation layout validation program,”IEEE/ACM Int. Conf. on Computer-Aided Design, pp. 322–325, 1988.
E.A. Emerson and A.P. Sistla, “Symmetry and model checking,”5th International Conference on Computer-Aided Verification, pp. 463–478, June 1993.
G.J. Holzmann,Automated Protocol Validation in Argos, Assertion Proving and Scatter Searching, Computer Science Press, pp. 163–188, 1987.
P. Huber, A.M. Jensen, L.O. Jepsen, and K. Jensen, “Towards reachability trees for high-level Petri nets,”Advances on Petri Nets, pp. 215–233, 1984.
C.N. Ip and D.L. Dill, “Better verification through symmetry,”Proc. 11th Int. Symp. on Computer Hardware Description Languages and Their Application, pp. 97–111, April 1993.
C.N. Ip and D.L. Dill, “Efficient verification of symmetric concurrent systems,”IEEE International Conference on Computer Design: VLSI in Computers and Processors, Cambridge, MA, pp. 230–234, October 3–6, 1993.
D. Lenoski, J. Laudon, K. Gharachorloo, A. Gupta, and J. Hennessy, “The directory-based cache coherence protocol for the DASH multiprocessor,”Proc. 17th Int. Symp. on Computer Architercture, pp. 148–159, 1990.
D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. Lam, “The Stanford DASH multiprocessor,”Computer, Vol. 25, No. 3, pp. 63–79, 1992.
B.D. Lubachevsky, “An approach to automating the verification of compact parallel coordination programs, I,”Acta Informatica, Vol. 21, No. 2, pp. 125–169, 1984.
J.M. Mellor-Crummey and M.L. Scott, “Algorithms for scalable synchronization on shared-memory multiprocessors,”ACM Transactions on Computer Systems, Vol. 9, No. 1, pp. 21–65, 1991.
H.B. Mittal, “A fast backtrack algorithm for graph isomorphism,”Information Processing Letters, Vol. 29, pp. 105–110, 1988.
G.L.Peterson, “Myths about the mutual exclusion problem,”Information Processing Letters, Vol. 12, No. 3, pp. 105–110, 1981.
P.H. Starke, “Reachability analysis of petri nets using symmetries,”Systems Analysis—Modelling—Simulation, Vol. 8, No. 4/5, pp. 293–303, 1991.
H.J. Touati, H. Savoj, B. Lin, R.K. Brayton, and A. Sangiovanni-Vincentelli, “Implicit state enumeration of finite state machines using BDDs,”IEEE Int. Conf. on Computer-Aided Design, pp. 130–133, 1990.
P. Wolper, “Expressing interesting properties of programs,”13th Annual ACM Symp. on Principles of Programming Languages, 1986.
P. Zafiropulo, C.H. West, H. Rudin, D.D. Cowan, and D. Brand, “Towards analyzing and synthesizing protocols,”IEEE Transactions on Communications, Vol. COM-28, No. 4, 1980.
Author information
Authors and Affiliations
Additional information
This research was supported by the “Multi-Module Systems” thrust of the Stanford Center for Integrated Systems, and by a gift from Mitsubishi Electronics Research Laboratories. Sun Microsystems provided computers.
Rights and permissions
About this article
Cite this article
Norris IP, C., Dill, D.L. Better verification through symmetry. Form Method Syst Des 9, 41–75 (1996). https://doi.org/10.1007/BF00625968
Issue Date:
DOI: https://doi.org/10.1007/BF00625968