Home // International Journal On Advances in Systems and Measurements, volume 7, numbers 1 and 2, 2014 // View article

State Space Reconstruction in UPPAAL: An Algorithm and its Proof

Authors:
Jonas Rinast
Sibylle Schupp
Dieter Gollmann

Keywords: State Space Reconstruction; On-line Model Checking; UPPAAL; Reference Counting; Use-Definition Chain.

Abstract:
Efficient state space reconstruction is necessary to carry out on-line model checking, a variant of model checking where parameters of a model are continually adjusted to remedy possible modeling faults. On-line model checking is, for example, useful in the medical domain where models of patient states and reactions are always inaccurate, but ensuring patient safety with model checking techniques is still desirable. In this paper, we propose a transformation reduction method based on use-definition chains to efficiently carry out the required state space reconstruction. We provide a formal specification of the general algorithm and proofs for its correctness. For evaluation we applied our reduction approach to the state space of the model checker UPPAAL. The experiments resulted in a reduction of the number of transformations necessary to reach a certain state by 42% on average.

Pages: 91 to 102

Copyright: Copyright (c) to authors, 2014. Used with permission.

Publication date: June 30, 2014

Published in: journal

ISSN: 1942-261x