电子发烧友App

硬声App

0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示
电子发烧友网>电子资料下载>嵌入式开发>基于模型检查的嵌入式软件验证方法解析

基于模型检查的嵌入式软件验证方法解析

2017-11-02 | rar | 0.5 MB | 次下载 | 1积分

资料介绍

嵌入式软件广泛应用于不同领域,如消费电子工业控制汽车电子、移动通信等。嵌入式软件的可靠性保证十分关键。嵌入式软件中常见的错误包括状态机错误、时序错误、栈溢出/存储溢出等,在开发过程中对嵌入式软件进行验证十分重要。
  对嵌入式软件的验证一般依赖于形式化的方法。
  形式化的方法可以对嵌入式软件系统进行严格的规约,并可以对系统进行不同视角的验证。验证主要是分析系统是否具有期望的性质。常见的验证技术主要有模型检查和定理证明。模型检查自动化程度高,并且当系统不具有期望性质时能给出反例,但它存在状态爆炸问题。定理证明能基于无穷状态空间分析,但是自动化程度不高,需要人工干预,并且在证明失败后不能给出易于理解的反例。本文使用符号模型检查技术来验证嵌入式软件系统,并通过触摸屏检测算法来说明该方法的应用。
  1 模型检查
  模型检查是一种验证有限状态系统的自动化技术,使用时序逻辑来描述系统性质。本文使用时序逻辑CTL来描述嵌入式系统满足的性质。CTL有分支时间和线性时间2种算子,其中分支时间算子是指路径量词A(“对所有计算路径”)和E(“对某些计算路径”),线性时间算子包括G(“always”,总是)、F(“somet:imes”,有时)、X(“next-time”,下一时刻)和U(“until”,直到)。其中线性时间算子G、F、X和U之前必须有1个路径量词。如图1所示,CTL公式用于描述有限状态系统上计算路径的相关性质。图1(a)表示EFg,即“存在一条计算路径,在某个状态,布尔量公式g为真”;图1(b)表示AFg,即“对所有计算路径,在每个计算路径的某个状态,布尔量公式g为真”;图1(c)表示EG,即“存在一条计算路径,在此路径的所有状态,布尔量公式g为真”;图1(d)表示AG,即“在所有计算路径的所有状态,布尔量公式g都为真”。
  基于模型检查的嵌入式软件验证方法解析
2 模型检查工具SMV
  常见的模型检查工具有贝尔实验室开发的SPIN、赫尔辛基工业大学计算机理论实验室开发的PR()D和MA—RIA、美国CMU计算机学院开发的SMV等。本文使用SMV作为对嵌入式软件验证的模型检查工具。
  SMV基于“符号模型检查”(Symbolic Model Claec-king)技术,开始是为了研究符号模型检查应用的可能性而开发的一种对硬件进行检查的实验工具,现在已经发展成为广为流行的分析有限状态系统的常用工具。
  本文中,软件系统模型用SMV语言描述。1个SMV程序由2部分组成:1个有限状态转换系统和1组CTL公式。SMV把初始状态和转换关系表示成二叉树图BDD(Binary Deciding Diagram),CTL公式表示系统模型的属性,也表示成BDD。通过模型检查算法遍历系统状态空间,给出1个声明的属性是正确或者不正确的验证结果,并给出1个不满足该属性的反例。1个CTL公式真正的值通过遍历状态图的方式确定,这种遍历的时间复杂性和状态空间大小、公式的长度成线性关系。
  3 触摸屏检测软件代码的验证
  触摸屏作为人机界面的输入设备已经广泛应用于各种嵌入式系统中,如手持设备、工业控制、车载设备等。对于有些应用,触摸屏是关键的输入设备,触摸屏失效会导致整个系统不可用。因此设计高效、清晰、可靠的触摸屏驱动程序非常重要。本文使用有限状态机来描述触摸屏检测算法,然后使用SMV语言来描述此有限状态系统模型,最后使用SMV工具对此模型进行验证。
下载该资料的人也在下载 下载该资料的人还在阅读
更多 >

评论

查看更多

下载排行

本周

  1. 1TC358743XBG评估板参考手册
  2. 1.36 MB  |  330次下载  |  免费
  3. 2开关电源基础知识
  4. 5.73 MB  |  6次下载  |  免费
  5. 3100W短波放大电路图
  6. 0.05 MB  |  4次下载  |  3 积分
  7. 4嵌入式linux-聊天程序设计
  8. 0.60 MB  |  3次下载  |  免费
  9. 5基于FPGA的光纤通信系统的设计与实现
  10. 0.61 MB  |  2次下载  |  免费
  11. 6基于FPGA的C8051F单片机开发板设计
  12. 0.70 MB  |  2次下载  |  免费
  13. 751单片机窗帘控制器仿真程序
  14. 1.93 MB  |  2次下载  |  免费
  15. 8基于51单片机的RGB调色灯程序仿真
  16. 0.86 MB  |  2次下载  |  免费

本月

  1. 1OrCAD10.5下载OrCAD10.5中文版软件
  2. 0.00 MB  |  234315次下载  |  免费
  3. 2555集成电路应用800例(新编版)
  4. 0.00 MB  |  33564次下载  |  免费
  5. 3接口电路图大全
  6. 未知  |  30323次下载  |  免费
  7. 4开关电源设计实例指南
  8. 未知  |  21548次下载  |  免费
  9. 5电气工程师手册免费下载(新编第二版pdf电子书)
  10. 0.00 MB  |  15349次下载  |  免费
  11. 6数字电路基础pdf(下载)
  12. 未知  |  13750次下载  |  免费
  13. 7电子制作实例集锦 下载
  14. 未知  |  8113次下载  |  免费
  15. 8《LED驱动电路设计》 温德尔著
  16. 0.00 MB  |  6653次下载  |  免费

总榜

  1. 1matlab软件下载入口
  2. 未知  |  935054次下载  |  免费
  3. 2protel99se软件下载(可英文版转中文版)
  4. 78.1 MB  |  537796次下载  |  免费
  5. 3MATLAB 7.1 下载 (含软件介绍)
  6. 未知  |  420026次下载  |  免费
  7. 4OrCAD10.5下载OrCAD10.5中文版软件
  8. 0.00 MB  |  234315次下载  |  免费
  9. 5Altium DXP2002下载入口
  10. 未知  |  233046次下载  |  免费
  11. 6电路仿真软件multisim 10.0免费下载
  12. 340992  |  191185次下载  |  免费
  13. 7十天学会AVR单片机与C语言视频教程 下载
  14. 158M  |  183278次下载  |  免费
  15. 8proe5.0野火版下载(中文版免费下载)
  16. 未知  |  138040次下载  |  免费