实时系统是指能够在指定或确定的时间内完成事件处理的计算机应用系统,其正确性不仅仅取决于其计算逻辑的正确性,并且与计算结果的产生时间有极大关系。在航空航天、生产控制、交通指挥、国防、核工业等安全攸关领域,实时系统发挥了至关重要的作用。因此保证实时系统的正确性和可靠性十分重要。模型检测是一种自动化地验证有限状态系统的技术。上世纪90年代,模型检测方法被应用到实时系统的可靠性和正确的检测上。模型检测针对的实时系统通常是封闭的,其运行结果只与系统自身的运行状态有关。然而在实际生活中,实时系统往往会间接或直接地受到外界因素的影响。因此我们需要合成一个控制器使得在外界因素影响下,系统仍然满足给定的性质,这就是控制器合成问题,它可以形式化的定义为:给定一个系统模型S和系统所需满足的性质Φ,是否存在一个控制器使得C(S)|=Φ。CTAV是一个基于时间自动机的实时系统模型检测工具。CTAV-TGA是在CTAV的基础上实现的以时间博弈自动机为模型的控制器合成工具。CTAV-TGA实现了以四种基本LTL性质<>p,[]p,[]<>p,<>[]p为获胜目标的控制器合成。但CTAV-TGA在语义完整性和实现效率上还存在一些不足,在本文中,根据时间博弈自动机中不变式和不可控动作的语义,改进了计算符号化状态的获胜信息方法,使得合成的控制器可以通过不可控的动作迁移到能够获胜的符号化状态上,完善了 CTAV-TGA的语义。另外还考虑了死锁结点,实现了对死锁状态信息的回溯,若初始状态通过不可控动作能够迁移到非获胜的死锁状态,表明控制器无法排除不可控动作的影响到达获胜状态,从而控制器算法能够提前终止。另外为了提高CTAV-TGA的效率,我们对四种基本性质的控制器合成算法进行了多核优化。