|
Bożena Woźna, Wojciech Zbrzezny
Reaching the limits for Bounded Model Checking
958
Abstract
The main contribution of the paper consists in showing
that the BMC method is feasible for ACTL*
(the universal fragment of CTL*) which subsumes both ACTL and LTL.
The extension to ACTL* is obtained by redefining
the function returning the sufficient number
of executions over which an ACTL* formula is checked,
and then by combining two known translations to SAT for ACTL and LTL
formulas. The proposed translation of ACTL* formulas is essentially
different from the existing translations of both ACTL and LTL formulas.
Moreover, ACTL* seems to be the largest set of temporal properties
which can be verified by means of BMC. We have implemented our new BMC
algorithm
for discrete timed automata and we have presented a preliminary
experimental
results, which prove the efficiency of the method.
The formal treatment is the basis for the implementation
of the technique in the symbolic model checker VerICS.
Keywords :
bounded model checking, logic ACTL* (ECTL*),
bounded semantics, translation to SAT, Discrete Timed Automata,
concrete model, abstract model, discretize model, system verification.
|
|
 |
 |
