A graph-based transformation reduction to reach UPPAAL states faster

Abstract

On-line model checking is a recent technique to overcome limitations of model checking if accurate system models are not available. At certain times during on-line model checking it is necessary to adjust the current model state to the real-world state and to do so in an efficient way. This paper presents a general, graph-based transformation reduction and applies it to reduce the length of transformation sequences needed to reach particular states in the model checker UPPAAL. Our evaluation shows that, generally, for the length of those sequences upper bounds exist independently from the elapsed time in the system. It follows that our proposed method is capable of fulfilling the real-time requirements imposed by on-line model checking. © 2014 Springer International Publishing Switzerland.