基于时间属性序列图的运行时验证技术研究

发布时间：2017-12-22 00:29

本文关键词：基于时间属性序列图的运行时验证技术研究　出处：《华中师范大学》2014年硕士论文　论文类型：学位论文

【摘要】：随着信息技术的发展,计算机技术已经融入了现代社会各个领域,得到极其广泛的应用。然而在这样的背景下,计算机系统的异常可能会造成灾难性后果。测试和仿真通常被用来保障这类安全关键系统的可靠性,但是这类方法针对的是实际运行前的系统,只能检测到系统的错误,而不能证明系统的正确。模型验证是完备的,但是它针对的是系统的抽象模型,难以证明系统的抽象模型和实际系统的等价性,同时这种方法需要遍历系统的所有执行路径,对于复杂系统来说,容易产生组合爆炸问题。与传统的测试和模型验证技术不同,运行时验证针对的是正在运行的实际系统。运行时验证一般采用时态逻辑来描述要验证的需求规约,并根据需求规约构造监控器。利用UML序列图来描述要验证的需求规约,克服了时态逻辑等形式化方法使用复杂的问题,使得普通的软件工程师也能方便正确的描述要验证的需求规约或性质。研究基于时间属性序列图(TPSD, Timed Property Sequence Diagram)自动生成监控器来进行运行时验证就显得十分有意义。本文提出了基于UML2.0时间属性序列图的运行时验证方法,其具体思想是使用时间属性序列图来描述要验证的需求规约,然后为序列图中的每个对象构造时间对象自动机,将整个序列图转换为时间自动机网络,以构造出运行时验证中所需的监控器,监控器监控目标系统的执行轨迹,判断目标系统的当前执行是否满足需求规约。本文先给出了满足本文验证需求的时间属性序列图形式化定义,接着提出了时间对象自动机及其形式化定义,然后提出了基于时间属性序列图的运行时验证方法的基本原理,进而提出了将时间属性序列图转化为时间自动机网络来构造预测监控器的算法。在此基础上,本文利用上述原理构造了一个基于时间属性序列图的运行时验证工具TPSD_monitor,构造了一个列控系统CTCS-2向CTCS-3级间切换仿真程序作为要验证的目标系统,利用该工具对构造的目标系统进行运行时验证,说明了本文中方法对安全关键系统进行运行时验证的可行性。进而进行了性能对比试验,实验表明,本文的监控器构造方法所产生的监控器运行开销较小,且能在一定程度上缓解监控器生成过程中的组合爆炸问题。
【学位授予单位】：华中师范大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP306

【参考文献】

中国期刊全文数据库前10条

1 曾光jf;;有限自动机基本模型及描述方法[J];电子技术;1988年01期

2 梁冰;刘群;;基于时间自动机网的C~3I系统建模和实时性验证[J];哈尔滨工程大学学报;2008年03期

3 孙玉强;刘三阳;王明斐;邹凌;;有限状态自动机的并行确定化及过程分析[J];计算机科学;2006年10期

4 周清雷,姬莉霞,王艳梅;基于UPPAAL的实时系统模型验证[J];计算机应用;2004年09期

5 张亚红;张琳琳;赵楷;陈佳丽;冯在文;;基于UML2.0序列图的Web服务运行时验证方法[J];计算机科学;2013年07期

6 柳毅;麻志毅;何啸;邵维忠;;一种从UML模型到可靠性分析模型的转换方法[J];软件学报;2010年02期

7 赵常智;董威;隋平;齐治昌;;面向参数化LTL的预测监控器构造技术[J];软件学报;2010年02期

8 张鹏程;李必信;李雯睿;;时间属性序列图:语法和语义[J];软件学报;2010年11期

9 张琛;段振华;田聪;;基于事件确定有限自动机的UML2.0序列图描述与验证[J];软件学报;2011年11期

10 张广红,陈平;关于AOP实现机制和应用的研究[J];计算机工程与设计;2003年08期