Trustworthy Systems

Tableaux for verification of data-centric processes

Authors

Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish

NICTA

Abstract

Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressivity for modelling rich data structures and reasoning about them in the course of a computation. To address this problem, we propose a rich modelling framework based on first-order logic over background theories (arithmetics, lists, records, etc) and state transition systems over corresponding interpretations. On the reasoning side, we introduce a tableau calculus for bounded model checking of properties expressed in a certain fragment of CTL* over that first-order logic. To overcome to some degree the limits of bounded model checking, we incorporate k-induction for proving safety properties.

BibTeX Entry

  @inproceedings{Bauer_BMN_13,
    address          = {Nancy, France},
    author           = {Bauer, Andreas and Baumgartner, Peter and Martin, Diller and Norrish, Michael},
    booktitle        = {Automated Reasoning with Analytic Tableaux and Related Methods},
    doi              = {10.1007/978-3-642-40537-2_5},
    editor           = {{Didier Galmiche and Dominique Larchey-Wendling}},
    keywords         = {model checking, first-order logic, business processes},
    month            = sep,
    pages            = {28--43},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6988.pdf},
    publisher        = {Springer},
    title            = {Tableaux for Verification of Data-Centric Processes},
    year             = {2013}
  }

Download