基于时间自动机的实时系统规范验证研究

摘要

实时系统不仅要求逻辑上是正确的,而且要求时间上也是正确的,这类系统在设计阶段需要进行严格的分析和验证.时间自动机是使用最为广泛的对实时系统进行规范验证的形式化方法之一.实时系统验证主要分为安全性验证和活性验证,系统的活性可以通过位置的不变式和转移的约束条件保证,验证也比较容易,本文对此不作过多讨论.安全性验证问题可归结为时间自动机的可达性分析,基于状态空间搜索的方法主要不足在于状态空间的大小随着过程数目的增加呈指数级递增,这就导致了状态空间爆炸问题.为了解决这个问题,我们必须构造时间自动机状态空间的有穷表示.本文主要研究了Alur提出的域自动机方法、带自动机方法以及Inhye Kang等提出的状态空间最小化方法,并在此基础上提出了时间段转换系统以及对状态空间的极小化方法.该方法用位置和进入位置的最大最小时钟值集合来表示状态而得到时间段转换系统,同时通过转换分析保留有效转换来简化这个转换系统.对简化后的系统,使用转换互模拟进行最小化.文中对该方法进行了可行性分析,通过与其它方法进行比较阐述了该方法的优点和不足,并建立了铁路交叉口控制门系统的最小化过程.在规范验证应用方面,本文研究了两种典型实时系统——道岔自动控制系统和自动筛选器系统.通过对系统进行分析和规范,给出了系统的时间自动机模型,并使用UPPAAL对模型进行验证,证明了系统的安全性、有效性和可控性.

目录

文摘

英文文摘

1前言

1.1研究背景

1.2研究现状

1.3研究内容

1.4本文结构

2时间自动机建模

2.1转换系统

2.1.1转换系统

2.1.2有时间约束的转换系统

2.2时间自动机

2.2.1语法和语义

2.2.2时间自动机积的构造

3可达性分析

3.1时间抽象转换系统

3.2域自动机

3.3带自动机

3.4我们的方法

3.4.1时间段转换系统

3.4.2时间段转换系统的最小化过程

3.4.3可行性分析

4自动机理论验证

4.1通过自动机空性验证

4.2时间语言理论

5基于UPPAAL的规范验证

5.1 UPPAAL介绍

5.2基于UPPAAL规范验证的应用

5.2.1自动筛选器系统

5.2.2道岔自动控制系统

5.3 UPPAAL的发展和前景

6总结与展望

致 谢

参考文献

附录1攻读硕士学位期间发表的论文