主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
杜德慧,昝慧,姜凯强,程贝.一种面向CPS的自适应统计模型检测方法.软件学报,2017,28(5):1128-1143
一种面向CPS的自适应统计模型检测方法
Self-Adaptive Statistical Model Checking Approach for CPS
投稿时间:2016-07-18  修订日期:2016-09-25
DOI:10.13328/j.cnki.jos.005216
中文关键词:  信息-物理融合系统  统计模型检测  抽象  学习  自适应性
英文关键词:cyber-physical system  statistical model checking  abstract  learning  self-adaptive
基金项目:国家自然科学基金(61472140,61170084);上海市自然科学基金(14ZR1412500)
作者单位E-mail
杜德慧 教育部可信软件国际合作联合实验室(华东师范大学), 上海 200062
可信软件国际联合研究中心(华东师范大学), 上海 200062
上海市高可信重点实验室(华东师范大学), 上海 200062 
dhdu@sei.ecnu.edu.cn 
昝慧 上海市高可信重点实验室(华东师范大学), 上海 200062  
姜凯强 上海市高可信重点实验室(华东师范大学), 上海 200062  
程贝 上海市高可信重点实验室(华东师范大学), 上海 200062  
摘要点击次数: 1368
全文下载次数: 1083
中文摘要:
      随着计算机与物理环境的交互日益密切,信息-物理融合系统(cyber-physical system,简称CPS)在健康医疗、航空电子、智能建筑等领域具有广泛的应用前景,CPS的正确性、可靠性分析已引起人们的广泛关注.统计模型检测(statistical model checking,简称SMC)技术能够对CPS进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPS的效率,是目前所面临的主要困难之一.针对此问题,首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法(Bayesian interval estimate,简称BIE)在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用主成分分析、前缀树约减等技术对仿真路径进行学习和抽象,以减少样本空间;然后,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题;最后,结合经典案例进行实验分析,实验结果表明,自适应SMC算法框架能够在一定误差范围内有效提高CPS统计模型检测的效率,为CPS的分析验证提供了一种有效的途径.
英文摘要:
      Cyber-Physical systems (CPSs) are advanced embedded systems engaging more interaction between computer and physical environment. CPSs are widely used in the field of healthcare equipment, avionics, and smart building. Meanwhile, the correctness and reliability analysis of CPSs has attracted more and more attentions. Statistical model checking (SMC) is an effective technology for verifying CPSs, which facilitates the quantitative evaluation for system performance. However, it is still a challenge to improve the performance of SMC with the expansion of systems. To address this issue, this study explores several SMC algorithms and concludes that Bayesian interval estimate is the most practical and efficient algorithm. However, large scale of traces are needed when the actual probability is around 0.5 during the evaluation. To overcome this difficulty, an algorithm, AL-SMC is proposed based on abstraction and learning techniques to reduce the size of sampling space. AL-SMC adopts some sophisticated techniques such as property-based projection, extraction and construction of prefix frequency tree. In addition, to improve the efficiency of SMC further, a framework of self-adaptive SMC algorithm, which uses the proper algorithm by probability prediction adaptively, is presented. Finally, the self-adaptive SMC approach is implemented with three benchmarks. The experimental results show that the proposed approach can improve the performance within an acceptable error range.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

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