近年来,随着科技的发展,各类移动机器人层出不穷,这些移动对象在其运行环境中自主移动,构成实时移动系统。运动规划是当前实时移动系统研究的热点方向之一,运动规划需要先对环境建模,然后基于模型制定相应的方法规划移动对象的运动过程。由于在各类建模方法中,形式化方法建模具有较高的可靠性和鲁棒性,因此本文将通过形式化方法建模实时移动系统的环境。在该模型基础上,本文以调度的方式宏观规划移动对象的运动过程,并利用可调度性分析判断移动对象运动过程的安全性,以保障实时移动系统的安全运行。本文的研究思路为:首先,在一种称之为“依赖结构”的形式化模型基础上增加时间元素,将其扩展为“时间依赖结构”以建模实时移动系统,同时结合界程构建移动事件,即将对象的移动转化为一系列进出界程的事件;其次,在时间依赖结构的基础上,制定基于移动事件的调度策略,并讨论移动对象的隔离关系,即通过对调度进行隔离分析判断两个指定移动对象是否发生碰撞;再次,讨论可调度性判定方法,以便通过可调度性分析判断系统运动规划结果的安全性,同时提出可调度性调度的生成方法,并设计算法加以实现;最后,引入根据时间依赖结构理论开发的原型系统（DSTool）,利用该工具对十字路口智能交通系统进行形式化建模并做对比实验。通过将本文调度理论与红绿灯调控情况下移动对象的出行延迟进行比较,结果显示,在本文调度理论调控下移动对象的出行延迟远小于在红绿灯调控下的出行延迟。除此之外,实验还显示调度理论调控下的出行延迟受车流量影响相对更小,这表明了根据本文调度理论调控的系统运行效率更高,运行过程更加稳定。本文主要创新点如下:（1）通过增加时间元素,把依赖结构扩展为时间依赖结构,同时还提出时间依赖结构的执行语义,使之能够建模实时性,具有更强的形式化表达能力;（2）提出适用于时间依赖结构的调度策略、可调度性分析方法以及可调度性调度的生成方法,并给出了相应的可调度性分析算法与调度生成算法,通过调度理论实现对移动对象路径的宏观规划;（3）利用基于本文提出的时间依赖结构理论开发的DSTool原型系统做对比试验,即模拟智能交通系统,将本文调度理论与红绿灯调度情况做对比,验证本文调度理论的可行性与效率。