| 实时调度问题的形式化描述及分析 |
| |
| 引用本文： | 涂刚,阳富民,卢炎生. 实时调度问题的形式化描述及分析[J]. 华中科技大学学报(自然科学版), 2004, 32(4): 47-49 |
| |
| 作者姓名： | 涂刚 阳富民 卢炎生 |
| |
| 作者单位： | 华中科技大学计算机学院,湖北,武汉,430074;华中科技大学计算机学院,湖北,武汉,430074;华中科技大学计算机学院,湖北,武汉,430074 |
| |
| 基金项目： | 国家高技术研究发展计划资助项目 (2 0 0 2AA4 4 5 0 10 ) |
| |
| 摘 要： | 使用自动机理论建立了一个用于分析实时调度问题的、可化简归并的形式化方法。通过分析单个任务的状态变化过程来构造实时系统的自动机。对自动机的状态进行化简和归并，大大降低了讨论实时调度问题的复杂度。以优先级上限协议为例构造了确定有穷自动机并使用该自动机证明了优先级上限协议的性质。
|
| 关 键 词： | 形式化方法 实时调度 优先级上限协议 自动机 |
| 文章编号： | 1671-4512(2004)04-0047-03 |
| 修稿时间： | 2003-07-14 |
The formal specification of real-time systems and its analysis |
| |
| Tu Gang Yang Fumin Lu Yansheng Doctoral Candidate, College of Computer Sci. , Tech.,Huazhong Univ. of Sci. , Tech.,Wuhan ,China.. The formal specification of real-time systems and its analysis[J]. JOURNAL OF HUAZHONG UNIVERSITY OF SCIENCE AND TECHNOLOGY.NATURE SCIENCE, 2004, 32(4): 47-49 |
| |
| Authors: | Tu Gang Yang Fumin Lu Yansheng Doctoral Candidate College of Computer Sci. & Tech. Huazhong Univ. of Sci. & Tech. Wuhan China. |
| |
| Affiliation: | Tu Gang Yang Fumin Lu Yansheng Doctoral Candidate, College of Computer Sci. & Tech.,Huazhong Univ. of Sci. & Tech.,Wuhan 430074,China. |
| |
| Abstract: | A formal method of specifying and analyzing real-time systems was presented based on automatic machine theory. The states of tasks were analyzed and the automatic machine of real-time system was constructed. By simplifying the automatic machine,a formal specification of corresponding real-time system was given,and the system in a more laborsaving way was analyzed. A scheduling algorithm called Priority Ceiling Protocol was specified by this method and the real-time system was analyzed. |
| |
| Keywords: | formal method real-time scheduling priority ceiling protocol automatic machine |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
