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

Real-time scheduling and schedulability analysis for mobile system

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

In order to ensure the safety of a complex real-time mobile system,the behavior of the mobile system needs to be modeled and analyzed by formal method.It is an important goal to judge whether the moving objects collide with each other during normal operation so as to verify the safety of a real-time mobile system.For achieving this goal,it is necessary to isolate and analyze each moving object within the system,which needs the supports from scheduling theory.However,traditional scheduling theory is based on coarse-grained task scheduling and cannot be directly used in fine-grained isolation analysis.To solve this problem,a mobile system can be modeled through Time Dependency Structure(TDS),which is a more fine-grained formal model based on events.The real-time scheduling method is defined on the basis of TDS,and the safety of the system can be judged by investigating the nature of real-time scheduling and analyzing the schedulability of isolation.