随着计算机技术的飞速发展，实时系统(real-timesystem)的应用日益广泛。在实际应用中，随着实时系统规模不断扩大、功能不断增强，嵌入其中的软件复杂程度也在迅速增加，从而导致实时系统运行时软件出现错误的可能性也在增加。实时系统软件运行过程中出现的任何一点差错将会导致巨额经济损失、时间浪费，甚至人员伤亡。为保证实时系统软件的正确性和安全性，提高其运行的可靠性，人们采取了许多的技术手段，其中形式化方法(formalmethods)起到了重要的作用。 一般来说，形式化验证(formalverification)技术包括关于规格说明性质的定理证明(theoremproving)技术和模型检查(modelchecking)技术。本文主要研究实时系统的模型检查技术。 模型检查的主要思想是构造系统的有限状态模型并穷尽搜索系统的整个状态空间以检查系统模型是否满足期望的性质。它有两种实施方案：时序逻辑模型检查和基于自动机理论的模型检查，它的关键问题是状态组合爆炸。 将基于自动机理论的模型检查技术作时间上的扩充可以验证实时系统。状态组合爆炸问题在实时系统模型检查中表现得更为突出。它不但来源于进程组合(processcomposition)和数据域(datadomain)，还来源于时间域(timedomain)。传统的优化技术只是从一定程度上缓解了状态爆炸，并不能从根本上解决问题，因为单机的内存和CPU的能力是有限的。 近年来，高性能计算技术飞速发展，为在一个小的实验室组建“个人超级计算机”提供了可能。本文提出了一种基于集群的实时系统模型检查技术，希望为从根本上解决状态组合爆炸问题提供一种新的途径。 我们选择时间自动机(TimedAutomata)描述实时系统的行为和性质，通过可达性分析算法验证系统模型是否满足期望的性质，用C++开发了一个串行实时系统模型检查器-RAModelChecker(ReachabilityAnalysisModelChecker)。 然后，我们结合高性能计算并行编程技术，引入动态负载平衡和On-the-fly技术，对RAModelChecker进行并行化处理，用C++和MPI(MessagePassingInterface)设计并实现了一个并行实时系统模型检查器—PRAModelChecker(ParallelReachabilityAnalysisModelChecker)。 最后，我们选择两个典型的实例对PRAModelChecker的性能进行分析。实验表明，将实时系统模型检查技术并行化是可行的，随着系统复杂性的增加，不但能提高工作效率，而且能处理的系统规模可伸缩，从而为从根本上解决状态组合爆炸问题提供了一种新的途径。