中文摘要：

模型检验是分析实时系统可靠性的一种重要手段。但其理论研究尚存在许多未解决问题，且与实际工业应用有很大差距。本项目旨在提高工业界系统的可靠性，桥接模型检验方法的研究与应用。主要完成了如下工作 1）设计基于概率时间自动机的概率线性时段不变集的检验算法设计。2）基于可决策的概率时间自动机，设计了概率线性发生不变集的模型检验算法。3）设计基于时间自动机的时段演算的模型检验算法。主要将线性时段不变集性质转化为对CTL 逻辑的检验。4）针对复杂系统，设计了将线性时段不变集性质转化为对CTL 逻辑的检验。并可用现有的模型检验工具UPPAAL进行检验。5）故障容错部件的设计和验证。6）利用模型检验和所定义的新的抽象关系进行零配置协议的形式建模和验证7)对三模冗余箭机系统的实例分析。进行模型和规范建立，包括安全性、活性、线性时段不变集等性质。8）针对实际的调度码头，设计集装箱下载的调度算法。并对此系统进行模型和规范建立。9)服务一致性的形式化分析及可信模型动环境下的建模和验证实例研究。