软件体系结构动态特征建模与验证

• 作者: 何坚 虞凡 覃征 贾晓琳
• 来源期刊: 西安交通大学学报
• 关键词: 软件体系结构 谓词/变迁网 线性时序逻辑 模型验证
• 年，卷（期）: 2005,（4）
• 页码范围: 347-350,355
• 页数: 5页
• 分类号: TP302.7
• 语种: 中文
• DOI: 10.3321/j.issn:0253-987X.2005.04.005

摘要

针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词/变迁(Pr/T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法.首先根据体系结构层次模型扩展Pr/T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质,最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性.所提方法结合了Pr/T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	覃征	西安交通大学电子与信息工程学院	158	2651	25.0	46.0
2	贾晓琳	西安交通大学电子与信息工程学院	23	240	8.0	15.0
3	虞凡	西安交通大学电子与信息工程学院	8	59	4.0	7.0
4	何坚	西安交通大学电子与信息工程学院	12	128	7.0	11.0