资料介绍
嵌入式软件广泛应用于不同领域,如消费电子、工业控制、汽车电子、移动通信等。嵌入式软件的可靠性保证十分关键。嵌入式软件中常见的错误包括状态机错误、时序错误、栈溢出/存储溢出等,在开发过程中对嵌入式软件进行验证十分重要。
对嵌入式软件的验证一般依赖于形式化的方法。
形式化的方法可以对嵌入式软件系统进行严格的规约,并可以对系统进行不同视角的验证。验证主要是分析系统是否具有期望的性质。常见的验证技术主要有模型检查和定理证明。模型检查自动化程度高,并且当系统不具有期望性质时能给出反例,但它存在状态爆炸问题。定理证明能基于无穷状态空间分析,但是自动化程度不高,需要人工干预,并且在证明失败后不能给出易于理解的反例。本文使用符号模型检查技术来验证嵌入式软件系统,并通过触摸屏检测算法来说明该方法的应用。
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 模型检查
模型检查是一种验证有限状态系统的自动化技术,使用时序逻辑来描述系统性质。本文使用时序逻辑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工具对此模型进行验证。
下载该资料的人也在下载
下载该资料的人还在阅读
更多 >
- 嵌入式软件之c语言编码规范 28次下载
- 嵌入式软件测试研究意义,嵌入式软件测试的研究
- 嵌入式软件测试参考书籍
- 基于FPGA嵌入式硬核的PCIExpress总线接口设计与验证
- 嵌入式应该如何学习?嵌入式学习方法和嵌入式学习路线资料说明
- 嵌入式软件方向的学习难点有哪些应该如何学习
- 嵌入式Linux与物联网软件开发C语言内核深度解析书籍的介绍
- 嵌入式系统死锁检测方法 0次下载
- 基于执行片段的嵌入式软件时序特性检测方法 0次下载
- 嵌入式软件时序异常检测 0次下载
- 嵌入式软件能耗模型ESPN 0次下载
- 嵌入式系统及其实时软件的开发 55次下载
- 基于CodeTEST的嵌入式软件测试技术
- 构造嵌入式系统软件的构件模型研究
- 基于模块化设计的嵌入式软件测试方法
- 嵌入式软件开发和软件开发的区别 1738次阅读
- 基于功能安全的汽车嵌入式软件单元验证技术研究 847次阅读
- 聊聊嵌入式软件分层 525次阅读
- 使用Zynq平台进行嵌入式软件和FPGA设计时有哪些挑战 476次阅读
- 嵌入式软件的设计模式(上) 1119次阅读
- 小型和受限嵌入式系统的固件验证 1304次阅读
- 嵌入式系统的全面解析 3146次阅读
- 基于CPLD实现嵌入式软件bootrom自动备份及切换功能的方法介绍 1177次阅读
- 基于嵌入式软件的JNI技术应用解析 1020次阅读
- 汽车嵌入式系统的设计过程、方法和测试工具框架浅析 1819次阅读
- 把软件项目管理方法引入嵌入式系统的开发之中的设计浅析 2034次阅读
- 嵌入式软件开发编程规范介绍 4206次阅读
- 嵌入式软件开发的这些编程规范你了解吗 3809次阅读
- 基于SCADE模型的高安全性嵌入式软件解决方案设计 2665次阅读
- 基于FPGA嵌入式系统的智能小车全面解析 9097次阅读
下载排行
本周
- 1TC358743XBG评估板参考手册
- 1.36 MB | 330次下载 | 免费
- 2开关电源基础知识
- 5.73 MB | 6次下载 | 免费
- 3100W短波放大电路图
- 0.05 MB | 4次下载 | 3 积分
- 4嵌入式linux-聊天程序设计
- 0.60 MB | 3次下载 | 免费
- 5基于FPGA的光纤通信系统的设计与实现
- 0.61 MB | 2次下载 | 免费
- 6基于FPGA的C8051F单片机开发板设计
- 0.70 MB | 2次下载 | 免费
- 751单片机窗帘控制器仿真程序
- 1.93 MB | 2次下载 | 免费
- 8基于51单片机的RGB调色灯程序仿真
- 0.86 MB | 2次下载 | 免费
本月
- 1OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234315次下载 | 免费
- 2555集成电路应用800例(新编版)
- 0.00 MB | 33564次下载 | 免费
- 3接口电路图大全
- 未知 | 30323次下载 | 免费
- 4开关电源设计实例指南
- 未知 | 21548次下载 | 免费
- 5电气工程师手册免费下载(新编第二版pdf电子书)
- 0.00 MB | 15349次下载 | 免费
- 6数字电路基础pdf(下载)
- 未知 | 13750次下载 | 免费
- 7电子制作实例集锦 下载
- 未知 | 8113次下载 | 免费
- 8《LED驱动电路设计》 温德尔著
- 0.00 MB | 6653次下载 | 免费
总榜
- 1matlab软件下载入口
- 未知 | 935054次下载 | 免费
- 2protel99se软件下载(可英文版转中文版)
- 78.1 MB | 537796次下载 | 免费
- 3MATLAB 7.1 下载 (含软件介绍)
- 未知 | 420026次下载 | 免费
- 4OrCAD10.5下载OrCAD10.5中文版软件
- 0.00 MB | 234315次下载 | 免费
- 5Altium DXP2002下载入口
- 未知 | 233046次下载 | 免费
- 6电路仿真软件multisim 10.0免费下载
- 340992 | 191185次下载 | 免费
- 7十天学会AVR单片机与C语言视频教程 下载
- 158M | 183278次下载 | 免费
- 8proe5.0野火版下载(中文版免费下载)
- 未知 | 138040次下载 | 免费
评论
查看更多