Parameteric model checking

Three Verics modules are aimed at parametric verification. Bounded Model Checking, a symbolic method based on encoding problems in propositional formulas and testing their SATisfiability, has been extended to deal with parametric properties. Input languages include:

  • 1-safe fragment of Elementary Net Systems (module PNTools);
  • 1-safe fragment of Time Petri Nets (module TPNTools);
  • UML State Machines (module UML2SAT).