Model-Checking

• Application of software tools designed for hardware CAD

  Verification by state space exploration - exhaustive on model
  

• Like earlier Prolog tool approach, but

  Forward search rather than reverse search
  
  Special algorithms (BDDs, etc.)
  A priori finite model (no unbounded recursion)
  Fully automatic once protocol is encoded

• Practicioners:

  Roscoe [Ros95], using FDR (the first)
  
  Mitchell, et al, using Murphi [MMS97]
  Marrero, et al, using SMV [MCJ97]
  Denker, et al, using Maude [DMT98]
  … and more

Previous slide

Next slide

Back to first slide

View graphic version