主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
桂盛霖,罗蕾,李允,于淼,徐建华.基于自动机理论的分布式实时调度分析工具.软件学报,2011,22(6):1236-1251
基于自动机理论的分布式实时调度分析工具
Schedulability Analysis Tool for Distributed Real-Time Systems Based on Automata Theory
投稿时间:2010-07-09  修订日期:2011-03-29
DOI:10.3724/SP.J.1001.2011.04015
中文关键词:  分布式系统  硬实时  调度性分析  行为自动机  环境自动机
英文关键词:distributed system  hard real-time  schedulability analysis  action automata  environment automata
基金项目:国家自然科学基金(90718019); 国家高技术研究发展计划(863)(2007AA010304); 国家“十一五”重点科技攻关项目(51315040106)
作者单位E-mail
桂盛霖 电子科技大学 计算机科学与工程学院,四川 成都 610054 shenglin_gui@uestc.edu.cn 
罗蕾 电子科技大学 计算机科学与工程学院,四川 成都 610054  
李允 电子科技大学 计算机科学与工程学院,四川 成都 610054  
于淼 西南交通大学 信息科学与技术学院,四川 成都 610031  
徐建华 西南交通大学 信息科学与技术学院,四川 成都 610031  
摘要点击次数: 6218
全文下载次数: 3954
中文摘要:
      分布式实时系统是广泛应用在众多关键领域的一类复杂实时系统.为保证其上运行任务的实时性,传统基于最坏响应时间的调度分析方法往往包含了实际系统运行过程中法达到的最坏情况,因此在这些情况下的分析结果过于悲观.基于自动机理论的模型检测方法的好处在于能够穷尽地搜索整个系统状态空间,得到精确的分析结果.为了利用形式化方法的优势来精确分析分布式系统上任务的调度性,建立了分布式系统上的任务形式化模型,提出了行为自动机和环境自动机以分别描述任务的执行语义及其外部到达关系,把任务的调度性分析转换为对自动机网络位置的可达性进行分析,证明了在某些调度策略下的调度性的可判定性,并给出了满足调度可判定性调度策略的条件和范围.基于上述结论,实现了一个支持分布式系统任务实时调度分析工具SCT(schedulability checking tool),并与其他工具进行了分析精确度和性能的比较.比较结果显示,SCT 可以提供最为精确的分析结果,但同时也具有最长的分析时间.
英文摘要:
      Distributed systems are complicated real-time systems, which have been used in many safety-critical domains. In order to ensure the real-time constraints over the tasks running on these systems, the traditional schedulability analysis techniques, based on worst-case response time analysis, usually consider the worst case which could never occur in real world applications, and therefore the obtained results are pessimistic. The model checking technique based on automata theory could exhaustively search the whole system state space and return precise results. By using formal methods to analyze the schedulability of tasks on distributed systems, this paper presents the formal task model on distributed systems. It uses action automata and environment automata to model the task execution semantics and the external event arrival patterns respectively. It also translates the schedulability analysis to the reachability analysis of the locations in automata network, and proves the decidability of schedulability under certain scheduling policies with attached conditions and scope. Based on these conclusions, the formal check model implements a schedulability check tool, SCT (schedulability checking tool), and compares it with other techniques and tools on accurateness and performance. The comparisons show that SCT always provides the most accurate results but with the longest execution time.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利