实时系统是一种要求反应或计算必须在规定时间内发生的系统。由于这些系统在工业及国防领域有着重要而广泛的应用，因此对这些系统进行形式化分析也成为近年来的一个研究热点。 随着社会的发展，尤其是网络的普及和应用，包括通讯协议和控制系统在内的越来越多的软件都以并发的方式运行，我们研究的就是这类带并发的实时系统。在对并发系统的研究中，传值和移动计算分别是两个不同的研究热点。在现有文献中，虽然对一些传统的基本并发系统都进行了实时扩充，得到了如Timed CCS，Timed CSP等实时演算，但尚未有能刻划实时传值系统的演算，而对移动演算，虽然有少数对π演算进行实时扩充的工作，但其语义是基于离散时间域的，并不能刻划时间在实数域上连续增长(流逝)等精确行为。 本文的研究工作主要由对实时传值系统和实时移动系统的建模和分析组成。 对于实时传值系统，本文的研究从计算模型与语义理论、分析与验证算法以及支持工具三个层面展开。在计算模型与语义理论方面着重探讨了带并发性的实时传值模型，定义了一个新的计算模型-时间符号迁移图(Timed Symbolic Transition Graph)，并建立了合适的语义理论。在分析与验证算法的设计方面，在新的计算模型基础上，我们分析了实时传值进程间各种不同互模拟的特点以及判定方法；尤其针对时间互模拟，根据符号互模拟的思想，本文给出了一个时间符号迁移图上的判定算法并证明了算法的正确性。在模型检测的算法方面，本文首先给出了时间符号迁移图上的一个可达性分析算法，随后还定义了能刻划更复杂性质的实时谓词μ演算并给出了检测这些性质的相应模型检测算法。为了有效地对连续时间进行表示和操作，本文针对通常使用的数据结构的范式化过程中出现的问题提出了一种新的信息消冗算法。在给出基本算法的基础上，我们构造了相应的验证工具-RealM，并在本文中给出了对限时重传协议进行的实例分析。 对于实时移动系统，本文对π演算进行了实时扩充，给出了实时π演算的语法和语义，并定义了该演算上的各种互模拟关系，以及相关的性质。本文不但证明了经典π演算的多数性质在新的模型下得到保持，还进一步给出了与时间有关的一些新的等式公理。最后，本文对实时π演算的一个有穷子集上的强实互模拟以及强互模拟均给出了完备的公理化结果。