摘要
使用自动机理论建立了一个用于分析实时调度问题的、可化简归并的形式化方法 .通过分析单个任务的状态变化过程来构造实时系统的自动机 .对自动机的状态进行化简和归并 ,大大降低了讨论实时调度问题的复杂度 .以优先级上限协议为例构造了确定有穷自动机并使用该自动机证明了优先级上限协议的性质 .
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.
出处
《华中科技大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2004年第4期47-49,共3页
Journal of Huazhong University of Science and Technology(Natural Science Edition)
基金
国家高技术研究发展计划资助项目 (2 0 0 2AA4 4 5 0 10 )
关键词
形式化方法
实时调度
优先级上限协议
自动机
formal method
real-time scheduling
priority ceiling protocol
automatic machine
