Statecharts及其时间扩展的形式化验证技术研究

摘要

模型检验是一种非常重要的自动验证方法，主要通过显式状态搜索或隐式不动点计算来验证有穷状态系统的模态命题性质，避免建立复杂的证明过程，并在不满足性质时能提供反例。二十多年来，人们对它进行了广泛而深入的研究，取得了许多研究成果，使得它在软硬件验证等方面得到广泛应用，受到了广大研究和开发人员的高度重视。 本文主要针对Statecharts及其时间扩展的形式化验证进行研究，研究工作包括：(1)通过对Statecharts和模型检验理论的研究，给出了平坦化和非平坦化的模型检验算法；(2)基于抽象解释框架的性质强保留的抽象模型检测；(3)把图形化的 Statecharts转换为义本表示的Statetxt，从而演绎验证Statecharts；(4)对连续时间扩展的Statecharts模型检验进行了研究和探索。主要成果表现在以下几个方面： ⑴通常模型检验Statecharts是先对其平坦化，然后使用已有模型检验工具进行验证。本文对传统的 Statecharts模型检验方法进行了改进，提出了一种针对Statecharts语义的平坦化模型检验方法。该方法基于Statecharts的操作语义和statecharts到LTS转换规则，得到标签转换系统LTS；在此基础上，对LTS进行符号表示，然后基于导向集的前向状态搜索算法，符号检验Statecharts模型是否满足CTL公式的性质。通过状态搜索的导向集和状态空间的符号表示，比较有效的缩减了需验证的状态窄间。为了进一步解决状态空间爆炸问题，又提出了一种非平坦化的模型检验方法，基于自动机理论及Statecharts的操作语义，避免构造平坦化过程，缩减状念窄间体积，并通过可达性分析和环路检测，直接对分层的Statecharts进行模型检验，验证其线性时态逻辑性质。非平坦化的方法能避免因Statecharts平坦化而引起的状态空间爆炸问题。 ⑵为了进一步研究Statecharts平坦化的模型检验方法，基于抽象解释的理论，以及完备抽象解释和性质强保留之间的关系，提出了一种性质强保留的抽象模型检验方法。此方法根据抽象解释中抽象域的最小完备精化，来获得CTL性质强保留的最优抽象模型，并且最优抽象模型总是存在。首先通过状态标签函数确定初始抽象域，然后通过不动点求解，得到对补集和标准前向转换完备的最优抽象域，也就是对CTL标准算子完备的最小抽象域，依据此抽象域求解CTL性质强保留的最优抽象状态划分。在抽象状态划分之间定义抽象转换关系，构造CTL性质强保留的抽象模型。并指出了抽象域对CTL标准算子是完备的当且仪当抽象域对补集和标准前向转换是完备的。此方法比较有效的解决了状态空间爆炸问题。 ⑶为了自动演绎验证Statecharts，需对图形化的Statecharts转换为文本表示Statetxt，然后进行验证。本文提出了一种在演绎验证不变式中辅助不变式的自动生成方法。描述了一个生成不变式和辅助谓词的框架，从而验证时态安全性质。为了保证搜索的收敛，通过对系统安全抽象来构造近似系统。该方法为形式化验证Statecharts提供了一种新的思路。 ⑷为了使Statecharts能描述连续时间的能力，本文精确定义了连续时间扩展的时间Statecharts，并提出了一种模型检验时间Statecharts的方法。采用项代数表示时间Statecharts和进程代数描述其并发行为，根据其一步语义及转换规则，把时间Statecharts映射为时间自动机，从而对时间Statecharts模型检的问题转换为对时间自动机的模型检验。为了克服了连续时间的无穷问题，通过抽象技术来获得有限状态空间，并给出了抽象精化的算法。

目录

文摘

英文文摘

声明

第一章 引言

1.1形式化验证

1.2形式化建模及Statecharts

1.3本文的主要研究内容

1.4本文的结构

第二章 模型检验

2.1模型

2.2逻辑

2.2.1线性时态逻辑(LTL)

2.2.2 μ-演算(面向动作的逻辑语言)

2.2.3计算树CTL逻辑的语法和语义

2.3模型检验

2.3.1基于自动机理论的模型检验方法

2.3.2基于语义的模型检验

2.3.3优化技术

2.4模型检验工具

2.5本章小结

第三章 平坦化的模型检验方法

3.1可视化规约语言Statecharts

3.2 Statecharts的一步语义

3.3基于层次自动机语义的模型检验方法

3.3.1层次自动机及其语义

3.3.2 Statecharts到层次自动机的转换

3.3.3 LTL性质的验证

3.4基于LTS的模型检验方法

3.4.1 Statecharts项语法

3.4.2 Statecharts一步语义的项表示

3.4.3基于LTS的Statecharts组合语义

3.5符号模型检验Statecharts

3.5.1 BDD和OBDD

3.5.2 LTS的符号化描述

3.5.3 Images和Pre-images操作

3.5.4向前状态搜索

3.5.5模型检验Statecharts

3.5.6实例分析

3.6本章小结

第四章 基于完备抽象解释的模型检验

4.1基础知识

4.1.1基础符号

4.1.2抽象解释

4.2抽象语义

4.3构造划分且强保留的抽象模型

4.3.1划分抽象

4.3.2强保留抽象

4.4闭包完备件与强保留

4.5实例分析

4.6本章小结

第五章 非平坦化的模型检验方法

5.1基本概念

5.2 LTL转换到LTS

5.3验证LTL件质

5.3.1可达性分析

5.3.2环路检测

5.3.3自动机判空

5.4实例分析

5.5本章小结

第六章 基于不变式的验证方法

6.1基础

6.1.1 Statetxt语言

6.1.2转换系统

6.1.3前置条件和后置条件

6.1.4不动点

6.2不变式

6.2.1前向传播

6.2.2后向传播

6.2.3双向传播

6.3安全性

6.3.1谓词图

6.3.2前向传播

6.3.3后向传播

6.4近似分析

6.5演绎验证Statecharts

6.6本章小结

第七章 模型检验时间Statecharts

7.1基本概念

7.1.1时钟和时钟约束

7.1.2时间自动机

7.1.3时间Statechans

7.2时间Statecharts项表示及其一步语义

7.2.1时间Statecharts项表示

7.2.2时间Statecharts的一步语义

7.3时间Statecharts到时间自动机转换

7.3.1时间Statecharts的转换规则

7.3.2宏步语义描述

7.3.3时间Statecharts转换为TA

7.4抽象验证

7.4.1抽象函数

7.4.2 TCTL抽象

7.4.3谓词集的基

7.4.4关于TCTL符号反例

7.4.5逐步渐增抽象精化算法

7.5本章小结

第八章 总结和展望

8.1论文总结

8.2未来工作展望

致谢

参考文献

附录