Bounded model checking

Bounded model checking (BMC) is one of the SAT-based (satisfiability checking) methods, and it was introduced as a technique complementary to the BDD-based symbolic model checking for LTL [BCC+99]. The main idea of BMC is to search for an execution (or a set of executions) of a system under consideration of some length k, which constitutes a counterexample for a tested property.

Let M be a model for a system S, and φ be an existential formula, describing a property P to be tested. All the BMC modules of VerICS perform the following algorithm.

A concrete realisation of Algorithm 1 depends on the function f and formulae [M](k,n) and [φ](M,k,n). The function f returns the number of paths of length k from the model M (i.e., the number of k-paths from the model M ) that are sufficient to evaluate the formula φ over the model M. The formula [M](k,n) represents all the possible sets of k-paths from the model M, and the formula [φ](M,k,n) encodes a number of constraints that must be satisfied on these sets for φ to be satisfied.

The efficiency of this method is based upon the observation that if a system is faulty, then often only a (small) fragment of its state space is sufficient for finding an error. Obviously, when testing large models and complex formulas the efficiency of the BMC method is dependent on the speed of the chosen SAT solver, on which the test is carried out. As SAT checkers have been progressively becoming more effective, the efficiency of BMC has improved, an observation experimentally demonstrated in, among others, [BCC+99,LP03,PWZ02a,PWZ02b].

Module 1 Reachability computation.

Module 1a The module is an implementation of a reachability method for Timed Automata without diagonal constraints (i.e., Diagonal Free Timed Automata - DFTA). The method is based on the BMC techniques. The details of the method can be found in [Zbrzezny04].

Module 1b The module is an implementation of a reachability method for Timed Automata with diagonal constraints (i.e., Diagonal Timed Automata). The method is also based on the BMC techniques. The details of the method can be found in [Zbrzezny05]. Both modules enable testing whether the given property is reachable or unreachable in the given network of Timed Automata by applying extended BMC algorithm [Zbrzezny05]. Module 1b can also be applied for Diagonal Free Timed Automata. However for DFTA Module 1a is more effective.

Module 2 - TECTL

The module concerns the BMC technique that is adapted to deal with real time systems, modeled via a network of communicating Diagonal Timed Automata, and properties expressed in the TECTL-G logic, a logic for real time. The main idea of this technique consists in a translation of the model checking problem for TECTL-G into the model checking problem of another logic, called ECTLy, and then applying a bounded model checking technique for ECTLy. The details of the method can be found in [WZ07].

Module 3 - TECTLK

The module concerns the BMC technique that is adapted to deal with multi-agent systems, defined as a set of communicating Timed Automata composed via parallel composition into a global Timed Automaton, and properties expressed in TECTLK, a logic for knowledge and real time. The main idea of this technique consists in a translation of the model checking problem for TECTLK into the model checking problem of another logic, called ECTLKy, and then applying a bounded model checking technique for ECTLKy. The details of the method can be found in [LWZ06, WLP05].

Module 4 - ECTL

The module is an implementation of the BMC technique that concerns untimed systems and the branching time properties expressed in ECTL (the existential fragment of CTL). The main modification of the original algorithm for LTL consists in a translation of a Kripke like model M to several symbolic paths, which can start at arbitrary states of the model. The details of the method can be found in [WPZ02].

Module 5 - ECTL*

The module is an implementation of the BMC technique that concerns untimed systems and the branching time properties expressed in ECTL* (the existential fragment of CTL*). The BMC technique for ECTL* is obtained by combining the BMC technique for ECTL with the technique for LTL. The details of the method can be found in [Wozna04].