实时和混成系统的模型确认算法及工具的研究

提出了一种新的实时和混成系统描述语言--混成规则表达式，在混成规则表达式的基础上给出了用线性规划方法验证混成自动机的统一算法，并加以实现；针对并发实时系统的形式模型--实时自动机网络，采用整数验证技术开发了一个检验线性时段性质的算法以攻击状态空间爆炸问题；基于整数时间验证技术解决了关于Time Petri Nets线性时段性质的验证问题，并且对一类Time Petri Nets提出用线性规划方法提高验证效率的途径；针对实时通讯应用领域，对目前广泛采用的Message Sequence Charts和UML Sequence Diagrams的验证问题进行了研究，解决了时间一致性验证问题；开发完成了一个实时和混成系统线性时段性质验证工具和一个实时和通讯系统时间一致性验证工具。