Automatic Verification Using Model and Module Checking

  • Roopak Sinha
  • Parthasarathi Roop
  • Samik Basu


As a precursor to system-level verification of SoCs, we present two well known verification techniques for closed and open systems respectively. Closed systems are “transformational” in nature and evolve without any need for external intervention. We present model checking, as an approach for the verification of closed systems. Open systems, in contrast, are “reactive” in nature and evolve based on interactions with an external environment. Typical applications of SoCs in the embedded system domain are open in nature. We present module checking as an automated technique for the verification of open systems. Both model checking and module checking are “formal” algorithms and hence require mathematical models to describe the system model (Kripke structures) and the desired properties (CTL).


Model Check Proof System Atomic Proposition Proof Obligation Kripke Structure 
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.


  1. [BRS07]
    S. Basu, P.S. Roop, R. Sinha, Local module checking for CTL specifications. Electron. Notes Theor. Comput. Sci. 176(2), 125–141 (2007)CrossRefGoogle Scholar
  2. [CGP00]
    E.M. Clarke, O. Grumberg, D. Peled, Model Checking (MIT Press, Massachusetts, 2000)Google Scholar
  3. [CC10]
    P. Cousot, R. Cousot, A gentle introduction to formal verification of computer systems by abstract interpretation. In Logics and Languages for Reliability and Security, ed. by J. Esparza, B. Spanfelner, O. Grumberg. NATO Science for Peace and Security Series - D: Information and Communication Security, vol 25 (IOS Press, Amsterdam, 2010), pp. 1–29Google Scholar
  4. [DKW08]
    V. D’Silva, D. Kroening, G. Weissenbacher, A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circuits Syst. 27(7), 1165–1178 (2008)CrossRefGoogle Scholar
  5. [CWCS11]
    F. Johnson, C. Chong-White, M. Millar, S. Shaw, Validating the realism and representativeness of SCATS in simulation. In 18th World Congress on ITS, 2011Google Scholar
  6. [KG99]
    C. Kern, M.R. Greenstreet, Formal verification in hardware design: A survey. ACM Trans. Design Autom. Electron. Syst. 4, 123–193 (1999)CrossRefGoogle Scholar
  7. [KV96]
    O. Kupferman, M.Y. Vardi, Module checking [model checking of open systems]. In Computer Aided Verification, 8th International Conference, CAV ’96 (Springer, Berlin, 1996), pp. 75–86Google Scholar
  8. [KV97]
    O. Kupferman, M.Y. Vardi, Module checking revisited. In Computer-Aided Verification, 7th International Conference, CAV ’97 (Springer, Berlin, 1997), pp. 36–47Google Scholar
  9. [KVW01]
    O. Kupferman, M.Y. Vardi, P. Wolper, Module checking. Inform. Comput. 164(2), 322–344 (2001)MathSciNetMATHCrossRefGoogle Scholar
  10. [RMK03]
    A. Roychoudhury, T. Mitra, S.R. Karri, Using formal techniques to debug the amba system-on-chip bus protocol. In DATE ’03: Proceedings of the Conference on Design, Automation and Test in Europe (IEEE Computer Society, Washington, 2003), p. 10828Google Scholar
  11. [oNSW]
    RTA Government of New South Wales, Accessed 11 Feb 2013
  12. [SR07]
    M. Satpathy, S. Ramesh, Test case generation from formal models through abstraction refinement and model checking. In A-MOST (ACM, New York, 2007), pp. 85–94Google Scholar
  13. [XZ03]
    N. Xu, Z. Zhou, Avalon bus and an example of SOPC system. Semicond. Technol. 28(2), 17–20 (2003)Google Scholar

Copyright information

© Springer Science+Business Media New York 2014

Authors and Affiliations

  • Roopak Sinha
    • 1
  • Parthasarathi Roop
    • 1
  • Samik Basu
    • 2
  1. 1.Electrical and Computer EngineeringThe University of AucklandAucklandNew Zealand
  2. 2.Department of Computer ScienceIowa State UniversityAmesUSA

Personalised recommendations