基于时间属性序列图的监控器构造方法

摘要：

运行时验证一般采用时态逻辑来描述要验证的需求规约,并根据需求规约构造监控器.这对于那些没有形式化经验的软件工程师而言,是一件非常困难的事情,同时,这类方法通常缺少时间机制支撑,因此难以满足实时系统运行时验证中的要求.序列图得到了广泛使用,研究基于序列图来自动生成监控器就显得十分有意义.提出基于UML2.0时间属性序列图的监控器的自动生成方法,其具体思想是使用时间属性序列图来描述要验证的需求规约,然后将整个序列图转换为时间自动机网络,构造出监控器.实验表明,该方法方便缺少形式化经验的软件工程师使用,所产生的监控器运行开销较小,能满足验证对实时性的要求,且有效缓解了监控器生成过程中的组合爆炸.

关键词：时间属性序列图、时间自动机、监控器、运行时验证

所属期刊栏目：36

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

资助基金：国家“九七三”重点基础研究发展计划课题项目2014CB340703

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

页数：共6页

页码：1426-1431