位置:成果数据库 > 期刊 > 期刊详情页
基于Event-B的中断管理需求和设计形式化建模与验证方法
  • ISSN号:1674-1579
  • 期刊名称:《空间控制技术与应用》
  • 时间:0
  • 分类:TP311[自动化与计算机技术—计算机软件与理论;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]北京控制工程研究所,北京100190, [2]北京轩宇信息技术有限公司,北京100190, [3]中国空间技术研究院,北京100190
  • 相关基金:国家自然科学基金资助项目(91118007,61632005)
中文摘要:

针对"重复加锁解锁"和"volatile修饰符误用"两种数据访问冲突缺陷模式,提出基于编码规则的检测方法.首先,对缺陷模式的故障机理进行分析,提炼出3条编码规则用以在开发阶段避免缺陷发生,并基于一个静态代码检查工具SpaceCCH进行了规则检测方法研究和实现.在实际星上软件上的实验结果表明,扩展的SpaceCCH能够高效、低误报、低漏报地发现规则违反,从而有效避免这两种的数据访问冲突问题.本文的贡献在于将一类复杂缺陷的检测转换为相应的编码规则及其检测.

英文摘要:

To solve pattern "double lock unlock"and pattern "misuse of volatile",a detection method based on coding rules is proposed. Firstly,the failure mechanism is analyzed,and then 3 coding rules are proposed to avoid corresponding defects in development stage. These rules and corresponding checking methods are researched and implemented by extending an existing static analysis tool named SpaceCCH. The evaluation result based on real world on-board software show that, the extended SpaceCCH can find rules violations efficiently with low false positive rate and low false negative rate,by which the data race bugs of pattern"double lock unlock"and pattern"misuse of volatile"can be avoided effectively. The main contribution of this paper is that the detection of a really complex bug is transformed to corresponding coding rules and their automatic detection.

同期刊论文项目
同项目期刊论文
期刊信息
  • 《空间控制技术与应用》
  • 中国科技核心期刊
  • 主管单位:中国航天科技集团公司
  • 主办单位:北京控制工程研究所
  • 主编:袁利
  • 地址:北京市5142信箱171分箱
  • 邮编:100194
  • 邮箱:aca@bice.org.cn
  • 电话:010-68111551 68111503
  • 国际标准刊号:ISSN:1674-1579
  • 国内统一刊号:ISSN:11-5664/V
  • 邮发代号:
  • 获奖情况:
  • 国内外数据库收录:
  • 中国中国科技核心期刊,中国北大核心期刊(2014版)
  • 被引量:841