《计算机学报》文章摘要   全文下载
文章题目	一种刻画功能和时间空间性能的统一验证模型atsFPM
作者	钮俊1)，2),3) 曾国荪1),2) 陈波1),2)
作者单位	1)(同济大学计算机科学与技术系 上海 201804) 2)(嵌入式系统与服务计算教育部重点实验室 上海 201804) 3)(浙江工商职业技术学院信息工程学院 浙江宁波 315012)
发表年份	2009
发表月份	4期(740—750)
文章摘要	摘要 对复杂信息系统的功能、性能进行组合验证，进而评估系统是否安全、可信，是当前的研究热点，但目前缺乏增加空间约束的验证模型.文章扩展已有的功能、性能验证模型，在状态空间上定义空间要求函数，提出一种刻画功能、时间和空间性能的统一验证模型atsFPM.给出基于正则式的路径范式描述信息系统行为的功能属性，给出atsFPM模型的语法和语义，构造路径范式与系统模型的积自动机，证明积自动机与原始模型在功能刻画、时间和空间描述上的等价，提出针对atsFPM的功能性能组合模型验证算法.实例分析表明，atsFPM统一验证模型能够有效解决信息系统功能和性能的组合分析问题，确保系统正确、安全、可信. 关键词 功能性能；空间约束；组合验证；安全可信 中图法分类号: TP301 DOI号: 10.3724/SP.J.1016.2009.00740