TY - CONF
T1 - Efficient temporal-logic query checking for presburger systems
T2 - Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering
Y1 - 2005
A1 - Zhang,Dezhuang
A1 - Cleaveland, Rance
KW - Formal Methods
KW - Model checking
KW - on-the-fly symbolic model checking
KW - Presburger systems
KW - query checking
AB - This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.
JA - Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering
T3 - ASE '05
PB - ACM
CY - New York, NY, USA
SN - 1-58113-993-4
UR - http://doi.acm.org/10.1145/1101908.1101915
M3 - 10.1145/1101908.1101915
ER -