Invariant checking method and apparatus using binary decision diagrams in combination with constraint solvers

摘要

An invariant checking method and apparatus using binary decision diagrams (BDDs) in combination with constraint solvers for determining whether a system property is an invariant of a system description. The invariant checking method receives system descriptions and system properties and transforms them into a model formula. Specific variables are eliminated from the model formula and a corresponding output formula is generated. The output formula is transformed into a logic formula by substituting a new logic variable for each integer constraint in the output formula. A constrained BDD is constructed from the logic formula. The constrained BDD uses a heuristic algorithm to order the logic variables in the paths leading to true or false. A constraint solver is applied to the integer constraints that correspond to the occurrences of logic variables in the BDD paths, which determines whether the system property is or is not an invariant of the system description.