The Research On The Verification Of Specifications With Associated Attributes In Graph Transformation Systems And Its Supporting Platform

Graph transformation systems are widely applied in software modeling and analysis phases. General graph transformation systems mainly use propositional temporal logic to specify the properties to be verified. However, propositional temporal logic cannot directly express the properties with associated attributes evolved over time. The paper proposes a novel approach which supports the verification of such properties with associated attributes in general graph transformation systems. It introduces a special indicator node and attributes as well as a set of rules to translate the properties with associated attributes into ordinary propositional temporal logic properties. Therefore, the associated properties can be verified accordingly. We illustrate our approach via two motivating examples and evaluate our approach with the popular graph based model checker: GROOVE. The result demonstrates the feasibility of our approach.However, the introduction of additional nodes will bring extra states during verification. By utilizing the technique of symmetry reduction and hierarchical structure, the model structure will be optimized so that it can decrease the state space and the temporal cost. Then we conduct comparative experiments by the two examples to demonstrate the efficiency of our approach.Moreover, to provide better usability, we use the Graphical Editing Framework(GEF) and the plug-in architecture of Eclipse to develop a supporting platform that embeds our proposed approach and can automatically introduce special indicator nodes for properties with associated attributes.