摘要
对于一个复杂的实时移动系统,为了确保其在运行过程中的安全性,需要通过形式化方法对其行为进行建模和分析。其中,判断各个移动对象在正常运行时是否互相碰撞是验证实时移动系统安全性的一个重要指标。为此,有必要对各个移动对象进行隔离分析,而隔离分析离不开调度理论的支持。然而,传统的调度理论是基于粗粒度的任务调度,不能直接用于细粒度的隔离分析。为了解决这一问题,可通过时间依赖结构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.
作者
陈聪
洪中
陈杨杨
张仕
蒋建民
CHEN Cong;HONG Zhong;CHEN Yang-yang;ZHANG Shi;JIANG Jian-min(College of Mathematics and Informatics,Fujian Normal University,Fuzhou 350117;College of Software Engineering,Chengdu University of Information Technology,Chengdu 610103,China)
出处
《计算机工程与科学》
CSCD
北大核心
2020年第9期1544-1555,共12页
Computer Engineering & Science
基金
国家自然科学基金(61772004,61175123)
福建省自然科学基金(2018J01777)。
关键词
移动性
隔离
调度策略
界程
mobility
isolation
scheduling policy
ambient