LeeTL: LTL with quantifications over model objects
Pouria Mellati, Ehsan Khamespanah, Ramtin Khosravi · 2017
Dynamic creating of objects and processes as one of the widely used techniques for developing models does not support by the majority of model checking tools. In addition, although there exist few model checking tools which support dynamic creation of model elements, e.g. Spin, they do not provide a property language for presenting the behavioral specifications of dynamically created elements. In this paper, we address this shortage and provide proper support for the model checking of object-based models which contain dynamic object creation. To this aim, we propose LeeTL, a new temporal logic that supports quantifications over model objects. Using LeeTL, it is also possible to traverse objects to access the variables of the objects for defining property formulas. We propose an algorithm for transforming LeeTL formulas to Büchi automata to be able to use the existing model checking tools which support Büchi automata.