Abstract
This paper presents and compares three techniques for mechanized verification of state-oriented design descriptions. The goal of this work is to gain insight into quantitative aspects of different modular verification techniques. One of the three verification techniques presented here is a traditional forward generation of a fixed point characterizing the reachable states. This does not utilize any modularity provided by the designer, and therefore it forms the basis for the comparison, whereas the two others do utilize such a modularity. One requires a substantial manual effort by the designer, but is computationally very efficient, while the other requires almost no manual assistance with a much better performance than the simple forward generation. The performance of the three techniques is compared on a set of examples.
Work supported by the Danish Technical Research Council, project Codesign.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Henrik R. Andersen. Partial model checking (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398–407, La Jolla, San Diego, 26–29 July 1995. IEEE Computer Society Press.
Henrik R. Andersen, Niels Maretti, and JØrgen Staunstrup. Partial model checking with ROBDDs. To appear in Proceedings of TACAS'97. LNCS.
R.E. Bryant. Graph-based algorithms for boolean function manipulation. Transactions on Computers, 8(C-35):677–691, 1986.
R.E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. Computing Surveys, 24(3):293–318, September 1992.
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proc. 1991 Int. Conf. on VLSI, August 1991.
K. Mani Chandy and Jajadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, volume 131 of LNCS, pages 52–71. Springer-Verlag, 1981.
Jo C. Ebergen and Ad M. G. Peeters. Design and analysis of delay-insensitive modulo-N counters. Formal Methods in Systems Design, 3(3), December 1993.
R.W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Proceedings of the Symposium in Applied Mathematics, volume 19, pages 19–32. American Mathematical Society, 1967.
Alan J. Hu, David L. Dill, Andreas J. Drexler, and C. Han Yang. Higherlevel specification and verification with BDDs. In G. v. Bochmann and D. K. Probst, editors, Proceedings of the 4th Workshop on Computer Aided Verification, CAV'92, June 29–July 1, 1992, Montreal, Quebec, Canada, volume 663 of LNCS, pages 82–95. Springer Verlag, 1992.
Jeffrey J. Joyce. Generic specification of digital hardware. In Designing Correct Circuits, Oxford 1990, pages 68–91. Springer-Verlag, 1991.
J.P. Billon and J.C. Madre. Original concepts of PRIAM, an industrial tool for efficient formal verification of combinational circuits. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, pages 487–501, Glasgow, Scotland, 1988. IFIP WG 10.2, North-Holland. IFIP Transactions.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
JØrgen Staunstrup. A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.
JØrgen Staunstrup and Niels Mellergaard. Localized verification of modular designs. Formal Methods in System Design, 6(3):295–320, June 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R., Staunstrup, J., Maretti, N. (1997). A comparison of modular verification techniques. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030625
Download citation
DOI: https://doi.org/10.1007/BFb0030625
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive