| 软件体系结构动态特征建模与验证 |
| 贾晓琳，覃 征，何 坚，虞 凡 |
| （西安交通大学电子与信息工程学院，710049, 西安）
|
| 摘要: 针对软件体系结构描述语言在分析、验证软件构架动态行为中的不足,采用谓词／变迁(Pr／T)网为软件体系结构动态行为建模,并提出了基于线性时序逻辑的软件体系结构动态行为模型验证方法. 首先根据体系结构层次模型扩展Pr／T网建立体系结构动态行为模型(DFM)并构造DFM的可达图,然后使用基于自动机理论的方法来验证模型的时态逻辑性质，最后通过对一个电子商务系统实例的并发控制机制建模和模型检测,验证了该方法的有效性. 所提方法结合了Pr／T网和线性时序逻辑的优点,为进一步开展软件体系结构动态行为的分析、验证奠定了基础. |
| 关键词: 软件体系结构;谓词／变迁网;线性时序逻辑;模型验证 |
| 中图分类号: TP302.7 文献标识码: A 文章编号: 0253-987X(2005)04-0347 |