摘要
Graph transformation is an important modeling and analysis technique widely applied in software engineer- ing. The attributes can naturally conceptualize the properties of the modeled artifacts. However, the lack of support for the specification of such attribute correspondence by ordi- nary propositional temporal logics hampers its further appli- cation during verification. Different from the theoretical in- vestigations on quantified second order logics, we propose a practical and light-weight approach for the verification of this kind of temporal specifications with associated attributes. Particularly, we apply our approach and extend the general- purpose graph transformation modeling tool： GROOVE. More- over, symmetry reduction techniques are exploited to reduce the number of states. Experiments with performance evalua- tions complement our discussion and demonstrate the feasi- bility and efficiency of our approach.
Graph transformation is an important modeling and analysis technique widely applied in software engineer- ing. The attributes can naturally conceptualize the properties of the modeled artifacts. However, the lack of support for the specification of such attribute correspondence by ordi- nary propositional temporal logics hampers its further appli- cation during verification. Different from the theoretical in- vestigations on quantified second order logics, we propose a practical and light-weight approach for the verification of this kind of temporal specifications with associated attributes. Particularly, we apply our approach and extend the general- purpose graph transformation modeling tool： GROOVE. More- over, symmetry reduction techniques are exploited to reduce the number of states. Experiments with performance evalua- tions complement our discussion and demonstrate the feasi- bility and efficiency of our approach.
