摘要： 为验证嵌入式实时系统开发过程中任务集的可调度性，设计并实现一种嵌入式系统调度分析工具。提出通用任务模型，建立任务与事件到达自动机和任务状态自动机的状态关系映射，利用基于模型检测的时间自动机可达性方法判定系统的可调度性。仿真实例结果表明，该工具的分析准确性较高。
关键词:
形式化方法,
时间自动机,
可调度性,
嵌入式实时系统,
任务模型
Abstract: 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.
Key words:
formalization method,
timed automata,
schedulability,
embedded real-time system,
task model
中图分类号:
于淼, 李允, 桂盛霖, 罗蕾. 基于时间自动机的嵌入式系统调度分析工具[J]. 计算机工程, 2012, 38(3): 290-292.
XU Miao, LI Yuan, GUI Cheng-Lin, LUO Lei. Schedule Analysis Tool for Embedded System Based on Timed Automata[J]. Computer Engineering, 2012, 38(3): 290-292.