软件体系结构环境中的行为规范说明与验证

摘要：

以实时线性时态逻辑作为逻辑框架,以时控自动机作为计算模型,扩展了软件体系结构环境Armani的行为规范说明与验证的能力.从而可以在体系结构描述的基础上从结构和行为两方面分析验证系统在体系结构层次上的重要性质,减少软件开发的风险;并且支持非完全规范说明,具有半形式化验证与组合验证的灵活性.

关键词：软件体系结构、行为规范、时控自动机

所属期刊栏目：29

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金60173103

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：8-10