主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
代声馨,洪玫,郭兵,杨秋辉,黄蔚,徐保平.多处理器实时系统可调度性分析的UPPAAL模型.软件学报,2015,26(2):279-296
多处理器实时系统可调度性分析的UPPAAL模型
Schedulability Analysis Model for Multiprocessor Real-Time Systems Using UPPAAL
投稿时间:2014-07-01  修订日期:2014-10-31
DOI:10.13328/j.cnki.jos.004781
中文关键词:  可调度性  模型检测  UPPAAL  多处理器实时系统  时间自动机
英文关键词:schedulability  model checking  UPPAAL  multiprocessor real-time system  timed automata
基金项目:国家自然科学基金(61332001, 61272104); 四川省应用基础研究项目(2014JY0112)
作者单位E-mail
代声馨 四川大学 计算机学院, 四川 成都 610065  
洪玫 四川大学 计算机学院, 四川 成都 610065 hongmei@scu.edu.cn 
郭兵 四川大学 计算机学院, 四川 成都 610065  
杨秋辉 四川大学 计算机学院, 四川 成都 610065  
黄蔚 四川大学 计算机学院, 四川 成都 610065  
徐保平 四川大学 计算机学院, 四川 成都 610065  
摘要点击次数: 3215
全文下载次数: 3054
中文摘要:
      随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.
英文摘要:
      As multiprocessor real-time systems are increasingly applied in safety critical systems, it's important to ensure the correctness of such systems. One key attribute of the correctness of real-time system is the schedulability that guarantees to satisfy the timing requirements. The traditional methods for determining the schedulability are either pessimistic or unsafe. To tackle the drawbacks of those methods, this paper proposes a scheme to achieve the schedulability analysis using model checking. It provides a schedulability analysis framework for multiprocessor real-time system. All the components involved in the schedulability of the system, including the tasks, the execution infrastructure and the dispatching management unit, are modeled as timed automata and implemented in UPPAAL. Further, UPPAAL is employed to verify whether the schedulability property is always satisfied. Symbolic model checking is applied to determine schedulability. However, because of the over-approximation for stopwatches, symbolic model checking cannot be used to disprove schedulability. As a supplement, statistical model checking is used to estimate the probability of non-schedulability and generate concrete counterexamples going along with non-schedulability. Statistical model checking is also used to obtain some performance information when system is schedulable.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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