摘要
为验证嵌入式实时系统开发过程中任务集的可调度性,设计并实现一种嵌入式系统调度分析工具。提出通用任务模型,建立任务与事件到达自动机和任务状态自动机的状态关系映射,利用基于模型检测的时间自动机可达性方法判定系统的可调度性。仿真实例结果表明,该工具的分析准确性较高。
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.
出处
《计算机工程》
CAS
CSCD
2012年第3期290-292,共3页
Computer Engineering
基金
国家自然科学基金资助项目(90718019)
国家"863"计划基金资助项目(2007AA010304)
