一种网构软件体系结构中的纵横验证机制

• 作者: 李长云 陈暄 高俊
• 来源期刊: 计算机应用研究
• 关键词: 形式化模型 形式化验证 软件体系结构 抽象状态机
• 年，卷（期）: 2012,（2）
• 所属期刊栏目: 软件技术研究
• 页码范围: 601-605
• 分类号: TP311
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2012.02.053

摘要

如何在开放、动态、复杂的Internet环境下开发网构软件是软件技术领域一个挑战性课题.从网构软件整个生命周期入手,对网构软件的形式化模型,在简单介绍抽象状态机(ASM)的基础理论之后,刻画了网构软件的构件模型,并对构件模型进行了基于ASM的形式化描述,在此基础上,将粗粒度抽象构件的精化问题转换为求解构件组合方案的问题,并在体系结构元层,提出一种双向验证方法对不同抽象程度的组合方案进行横向和纵向的验证,以保证目标系统的正确性和求精过程的正确性.以上形式化建模和双向验证方法尽可能地避免和消除了软件设计早期的错误.通过系统实验验证可以看出,该方法对网构软件的开发具有一定指导意义.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李长云	湖南工业大学计算机与通信学院	130	747	12.0	21.0
2	高俊		9	39	5.0	6.0
3	陈暄		39	80	5.0	7.0