基于概率时间自动机的概率时段演算的模型检验及应用研究

模型检验是分析实时系统可靠性的一种重要手段。但其理论研究尚存在许多未解决问题，且与实际工业应用有很大差距。本项目将首先扩充模型检验算法：基于概率时间自动机，研究概率线性时段不变集性质的模型检验算法，并研究能处理更通用的概率时段演算性质的算法；同时研究基于概率时段自动机的概率时段演算性质的模型检验算法以降低算法复杂性，以及可以模型检验模糊性质的算法等。并进一步将研究结果应用于个人网络和航空航天系统。分别研究解决个人网络的"服务和上下文发现协议"、星务系统的"多CPU切换协议"和箭机系统的"表决器和仲裁协议"所面临的问题，提高通讯网络与航天系统的可靠性。. 课题目的是桥接模型检验方法的研究与应用。现代工业竞争已经发展为协议标准主导权的竞争，模型检验可增强协议的正确性与完备性，增强我国工业界制定协议标准的能力。在航空航天领域的应用可增强系统的安全、可靠性，推动国防科技的发展。