计算机工程与应用2016，Vol.52Issue(12)：15-18,4.DOI:10.3778/j.issn.1002-8331.1407-0311
新型属性图文法反应式规约验证方法
Novel approach for attributed graph grammar response specification verifi-cation
摘要
Abstract
Attribute graph grammar is widely used in modeling and analysis in software design phase. However, ordinary propositional temporal logic cannot directly express the response specification with associated attributes. This paper proposes a novel approach which supports the verification of such properties with associate attributes in general graph grammar transformation systems. It introduces a special indicator node and attributes as well as a set of rules to translate the properties into common propositional temporal logic properties. Therefore the corresponding properties can be verified. It illustrates the approach via a motivating example with the popular graph based model checker GROOVE. The result demonstrates the feasibility of this approach.关键词
属性图文法/模型检测/关联属性Key words
attribute graph grammar/model checking/associate attributes分类
信息技术与安全科学引用本文复制引用
黄延凯,周宇,魏欧..新型属性图文法反应式规约验证方法[J].计算机工程与应用,2016,52(12):15-18,4.基金项目
国家自然科学基金（No.61202002，No.61170043）；中央高校基本科研业务专项资助（No.NS2012135）。 （）
