移动系统的实时调度与可调度性分析

摘要

对于一个复杂的实时移动系统,为了确保其在运行过程中的安全性,需要通过形式化方法对其行为进行建模和分析.其中,判断各个移动对象在正常运行时是否互相碰撞是验证实时移动系统安全性的一个重要指标.为此,有必要对各个移动对象进行隔离分析,而隔离分析离不开调度理论的支持.然而,传统的调度理论是基于粗粒度的任务调度,不能直接用于细粒度的隔离分析.为了解决这一问题,可通过时间依赖结构T DS模型来建模移动系统.该模型是基于事件的更细粒度的形式化模型,通过在时间依赖结构的基础上定义实时调度的方法,进而讨论实时调度的性质并进行隔离的可调度性分析,能够判断系统在运行过程中的安全性.