Graph transformation systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a ...Graph transformation systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software development.But even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their requirements.In this paper,we present a new solution to verify graph transformation systems using the Bogor model checker.The attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph rules.Experimental results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.展开更多
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 s...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 systems have become a general formal modeling language to describe many models in software development process.Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software development.But even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their requirements.In this paper,we present a new solution to verify graph transformation systems using the Bogor model checker.The attributed graph grammars(AGG)-like graph transformation systems are translated to Bandera intermediate representation(BIR),the input language of Bogor,and Bogor verifies the model against some interesting properties defined by combining linear temporal logic(LTL) and special-purpose graph rules.Experimental results are encouraging,showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.
文摘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.
