基于LTL的软件可信性指标分析方法研究

摘要

随着计算机硬件技术和相关软件技术日益成熟，软件在人们日常生产生活中扮演着越来越重要的角色，并在工业、通讯业、医疗、军事和航空航天等方面也得到了广泛的应用。软件系统在很多重要领域的应用使得这些领域对软件系统的依赖不断增加，这就使得计算机的应用环境变得更加复杂，比如软件系统的规模变得越来越大，复杂度也变得越来越高。但是，计算机软件不可避免的存在着各种漏洞，这将严重影响人们在生产和生活中的各项活动。因此，提高软件的可信性和正确性，构建高可信性软件已经成为了近几年软件研究开发方向的热点问题。运行时验证作为一种轻量级的验证技术可以作为传统验证技术的有效补充，这也使得运行时验证技术在软件可信性的领域中得到了广泛的应用。它的主要特点是在软件系统的运行过程中进行验证，这也为实时纠正软件错误奠定了基础。
　　本文对软件可信性运行时验证理论进行了细致的分析研究，对运行时验证的线性时序逻辑（Linear Temporal Logic，以下简称LTL）、自动机理论和运行时验证工具等部分进行了分析研究。针对运行时验证监控器的构造，本文采用了运行时验证工具面向方面编程中的JavaAOP技术和AspectJ技术实现了监控器的设计，这种方法基于自动机转化算法，利用自动机转化方法将语义表达的属性转化为运行时验证监控器。其中，使用JavaAOP技术实现了对软件系统的函数进行运行时的监控，使用AspectJ技术实现了对软件系统的变量进行运行时的监控。并具体实现了监控代码插装及事件、条件计算等问题。
　　本文实验在Windows操作系统平台下对文中提到的运行时验证监控器进行具体实现，实验表明，该监控器在实现对软件系统中函数和变量进行运行时监控的同时也兼顾了软件运行速度等问题。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 绪论

1.1 课题研究背景及意义

1.2 软件可信性及运行时验证的研究现状

1.3 研究目标与内容

1.4 论文的组织结构

第2章 运行时验证理论

2.1 运行时验证形式化语义

2.2 自动机理论

2.3 运行时验证实现工具

2.4 本章小结

第3章 基于移动时间的线性时序逻辑

3.1 真值域和语法语义

3.2 作用在有限轨迹上的线性时序逻辑

3.3作用在无限轨迹上的线性时序逻辑

3.4基于三值语义的线性时序逻辑

3.4 本章小结

第4章 运行时验证监控器构造与可信性指标分析

4.1 逻辑、语言与自动机

4.2 基于LTL3的监控器构造

4.3 代码插装和条件计算

4.4 软件可信性指标分析

4.5 本章小结

第5章 实验及结果分析

5.1 实验目的

5.2 实验平台及环境

5.3 实验过程

5.4 实验结果分析

5.5 软件可靠性指标分析

5.6 本章小结

结论

参考文献

攻读硕士期间发表的文献和取得的科研成果

致谢