导　　师： 周清雷

学科专业： H1202

授予学位： 硕士

作　　者： ;

机构地区： 郑州大学

摘　　要： 本文在R.ALUR等人提出的时间自动机的基础上深入研究了系统模型验证理论及其实际应用。通过判定实时系统以及它的规范说明所对应的时间正则语言的交集是否为空对实时系统进行规范验证，比较常用的验证方法包括构造区域自动机和带自动机。通过对这些方法分析研究，发现当系统规模较大时，规范建模过程就会相对复杂，而且还可能会出现状态组合爆炸的问题。因此，系统需要一种能较好解决这些问题的自动规范验证技术。 本文对快速前向验证算法进行改进，提出了一种带有启发性信息的快速前向验证算法。文中设计估价函数用于估算每一个全局状态到达目标全局状态需要付出的代价，定义无用状态循环用来避免对无用状态重复分析，这样既节省了系统存储空间，又提高了求解问题的效率。接下来，本文对一个通讯协议进行分析和规范，并且利用UPPAAL对该协议的时间自动机模型进行自动规范验证，证明了协议的正确性和安全性。 　　本文利用将时延PETRI网转换到时间自动机的语义等价转换算法，将一个带有单处理器的铁路岔道系统的时延PETRI网模型转换成与其语义等价的一组时间自动机模型，并且利用UPPAAL对转换后系统模型的安全性和受限活性进行自动规范验证。

关 键 词： 实时系统 时间自动机 协议验证 时延 网 模型验证理论

分 类 号： [TP311.5]

领　　域： [自动化与计算机技术] [自动化与计算机技术]