检索
E-mail
RSS
作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2012, Vol. 38 ›› Issue (3): 290-292.doi: 10.3969/j.issn.1000-3428.2012.03.095

• 开发研究与设计技术 • 上一篇    

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

于 淼1，李 允2，桂盛霖2，罗 蕾2   

  1. (1. 西南交通大学信息科学与技术学院，成都 610031；2. 电子科技大学计算机科学与工程学院，成都 610054)
  • 收稿日期:2011-07-15 出版日期:2012-02-05 发布日期:2012-02-05
  • 作者简介:于 淼(1985－)，男，硕士，主研方向：嵌入式系统，实时软件建模；李 允，副教授、博士；桂盛霖，博士；罗 蕾，教授、博士生导师
  • 基金项目:
    国家自然科学基金资助项目(90718019)；国家“863”计划基金资助项目(2007AA010304)

Schedule Analysis Tool for Embedded System Based on Timed Automata

YU Miao 1, LI Yun 2, GUI Sheng-lin 2, LUO Lei 2   

  1. (1. School of Information Science & Techology, Southwest Jiaotong University, Chengdu 610031, China; 2. School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu 610054, China)
  • Received:2011-07-15 Online:2012-02-05 Published:2012-02-05

PDF

1368

被引次数

3

摘要： 为验证嵌入式实时系统开发过程中任务集的可调度性，设计并实现一种嵌入式系统调度分析工具。提出通用任务模型，建立任务与事件到达自动机和任务状态自动机的状态关系映射，利用基于模型检测的时间自动机可达性方法判定系统的可调度性。仿真实例结果表明，该工具的分析准确性较高。

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

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

中图分类号: