期刊论文

中文

小型微型计算机系统

1000-1220

2015

36

7

1426-1431

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

本校为第一机构

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

Runtime verification generally uses temporal logic to describe the requirement specifications to be verified and constructs monitors on the basis of requirement specifications. However,it is difficult for those software engineers who do not have any formal experience to use temporal logic to describe the requirement specifications. It is also difficult to meet the requirements of the real-time systems because the approach lacks time mechanisms. Sequence diagrams are commonly used to describe the requirement specifications,So the research of generating monitors automatically based on the timed ...