摘要
提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.
Hypergraphs with constraints was proposed to represent software architectures.The formal semantics and operations of dynamic evolution production rules of software architectures were presented based on hypergraph morphisms.A software architecture style was defined as a type hypergraph,and the dynamic evolution of software architectures was modeled by applying hypergraph grammars and the architecture style.Model checking technique was used to verify the correctness of dynamic evolution of software architectures,an algorithm was designed to verify the property of dynamic evolution of software architectures.Experimental analysis was made by using a model checker.The approach provides a graphical representation of dynamic evolution of software architectures,and displays a formal theoretical framework based on grammars.
出处
《同济大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2011年第5期745-750,共6页
Journal of Tongji University:Natural Science
基金
国家"八六三"高技术研究发展计划(2007AA01Z425
2009AA012201)
国家"九七三"重点基础研究发展规划(2007CB316502)
国家自然科学基金(90718015)
NSFC-微软亚洲研究院联合资助(60970155)
教育部高等学校博士学科点专项科研(20090072110035)
上海市优秀学科带头人计划(10XD1404400)
高效能服务器和存储技术国家重点实验室开放基金(2009HSSA06)
关键词
软件演化
体系结构
形式化建模
模型检测
software evolution
architecture
formal modeling
model checking
