Abstract: 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.

Key words: mobility, isolation, scheduling policy, ambient