基于自动机理论的分布式实时调度分析工具

• 作者: 于淼 徐建华 李允 桂盛霖 罗蕾
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 分布式系统 硬实时 调度性分析 行为自动机 环境自动机
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 形式化方法与工具专刊
• 页码范围: 1236-1251
• 分类号: TP311
• 字数: 14218字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.04015

摘要

分布式实时系统是广泛应用在众多关键领域的一类复杂实时系统.为保证其上运行任务的实时性,传统基于最坏响应时间的调度分析方法往往包含了实际系统运行过程中无法达到的最坏情况,因此在这些情况下的分析结果过于悲观.基于自动机理论的模型检测方法的好处在于能够穷尽地搜索整个系统状态空间,得到精确的分析结果.为了利用形式化方法的优势来精确分析分布式系统上任务的调度性,建立了分布式系统上的任务形式化模型,提出了行为自动机和环境自动机以分别描述任务的执行语义及其外部到达关系,把任务的调度性分析转换为对自动机网络位置的可达性进行分析,证明了在某些调度策略下的调度性的可判定性,并给出了满足调度可判定性调度策略的条件和范围.基于上述结论,实现了一个支持分布式系统任务实时调度分析工具SCT(schedulability checking tool),并与其他工具进行了分析精确度和性能的比较.比较结果显示,SCT可以提供最为精确的分析结果,但同时也具有最长的分析时间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李允	电子科技大学计算机科学与工程学院	25	207	9.0	13.0
2	罗蕾	电子科技大学计算机科学与工程学院	58	583	14.0	21.0
3	桂盛霖	电子科技大学计算机科学与工程学院	13	85	6.0	9.0
4	徐建华	西南交通大学信息科学与技术学院	6	23	2.0	4.0
5	于淼	西南交通大学信息科学与技术学院	6	26	3.0	5.0