基于时间自动机的嵌入式系统调度分析工具  

Schedule Analysis Tool for Embedded System Based on Timed Automata

作　　者：于淼[1] 李允[2] 桂盛霖[2] 罗蕾[2] 

机构地区：[1]西南交通大学信息科学与技术学院,成都610031 [2]电子科技大学计算机科学与工程学院,成都610054

出　　处：《计算机工程》2012年第3期290-292,共3页Computer Engineering

基　　金：国家自然科学基金资助项目(90718019);国家"863"计划基金资助项目(2007AA010304)

摘　　要：为验证嵌入式实时系统开发过程中任务集的可调度性,设计并实现一种嵌入式系统调度分析工具。提出通用任务模型,建立任务与事件到达自动机和任务状态自动机的状态关系映射,利用基于模型检测的时间自动机可达性方法判定系统的可调度性。仿真实例结果表明,该工具的分析准确性较高。In order to verify the schedulability property of the task set in embedded real-time system, this paper designs and implements a schedulability analysis tool. It abstracts general task model in the first place and defines the logical mapping of task models in system to states of two types of timed automata. Based on model checking theory, this tool determines whether this system can be scheduled by timed automata reachability method, and finally tests the accuracy of that method through two simulation examples.

关 键 词：形式化方法 时间自动机 可调度性 嵌入式实时系统 任务模型 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]