基于模型检查的嵌入式软件构件化分析与验证.pdf

《基于模型检查的嵌入式软件构件化分析与验证.pdf》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于模型检查的嵌入式软件构件化分析与验证2015年1月中图分类号：TP311.5UDC分类号：004.4基于模型检查的嵌入式软件构件化分析与验证作者姓名孙福振学院名称计算机学院指导教师廖乐健教授答辩委员会主席陈群秀教授申请学位工学博士学科专业计算机应用学位授予单位北京理工大学论文答辩日期2015年1月基于模型检查的嵌入式软件构件化分析与验证作者姓名孙福振学院名称计算机学院指导教师廖乐健教授答辩委员会主席陈群秀教授申请学位工学博士学科专业计算机应用学位授予单位北京理工大学论文答辩日期2015年1月Mod

2、elCheckingBasedFormalAnalysisandVerificationforComponentOrientedEmbeddedSoftwareCandidateName：FuzhenSunSchoolorDepartment:ComputerScienceFacultyMentor:LejianLiaoChair,ThesisCommittee:QunxiuChenDegreeApplied:DoctorofPhilosophyMajor:ComputerandApplication

3、Degreeby:BeijingInstituteofTechnologyTheDateofDefence：January2015研究成果声明本人郑重声明：所提交的学位论文是我本人在指导教师的指导下进行的研究工作获得的研究成果。尽我所知，文中除特别标注和致谢的地方外，学位论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得北京理工大学或其它教育机构的学位或证书所使用过的材料。与我一同工作的合作者对此研究工作所做的任何贡献均已在学位论文中作了明确的说明并表示了谢意。特此申明。签名：日期：北京理工

4、大学博士学位论文摘要伴随着近年来计算机硬件设备性能的迅速提升以及嵌入式系统的广泛应用，嵌入式软件的复杂度和规模也不断膨胀，软件的可靠性占据了整个系统的统治性地位。因此，嵌入式软件的设计方法和可靠性保障已经成为近几年软件工程师和计算机科学研究者所共同关心的热点问题。传统的嵌入式软件设计方法已经难以适应现代高复杂性和大规模的嵌入式软件面临的高可靠性、资源约束、面向特定领域等需求，必须借鉴和引入软件工程中构建复杂软件系统的理论和方法。基于构件化的软件设计方法作为软件工程主流之一，已逐渐被应用到复杂嵌入式软件

5、设计中来，大大提高了软件开发效率和软件功能可重用性。嵌入式系统通常是由面向特定领域的具有各自独立的计算子模块组成，具有较高的构件化特征，通过构件与构件之间的交互运行来完成嵌入式软件的特定功能。针对产业界广为使用的构件化设计模型是UML顺序图，以此来描述系统运行中各个构件交互的场景，作为一种非形式化建模方法具有与生俱来的缺陷即难以进行自动化分析和验证问题。本论文深入地研究了嵌入式软件构件交互协议建模的需求，对复杂嵌入式软件系统提出了以数据库为底层支撑的基于一阶逻辑和承诺理论的构件交互协议模型，并给出了与

6、之对应的基于模型检查的数据流敏感的构件交互协议和带资源约束目标的构件交互协议的分析与验证方法。本论文的主要工作和贡献如下：(1)针对构件化嵌入式软件系统，提出了以数据库为底层支撑的基本构件交互协议模型，除了描述构件动作的输入/输出消息签名外，利用一阶逻辑规则给出构件动作的输入数据约束规则、控制流规则、输出规则和状态转换规则，使得构件之间的交互运行得以全面的形式化描述，使得构件交互协议的自动化分析和验证成为可能。(2)为赋予嵌入式软件的构件交互协议以面向特定领域的业务语义，本论文在上述基本构件交互协议模

7、型的基础上进行语义扩展，并给出了引入承诺理论的业务构件协议模型。该模型利用面向特定领域的业务词汇对嵌入式软件构件动作的业务效果进行标注，除了包括直接效果还允许标注以间接的承诺效果，自然地建模了嵌入式软件构件与底层支撑硬件之间的契约行为。(3)为能形式化描述和分析验证嵌入式软件构件交互运行的动态行为，本论文研究了基本构件交互协议模型的线性一阶逻辑（First-OrderLinearTemporalLogic，I北京理工大学博士学位论文FO-LTL）性质验证问题。FO-LTL公式可表达基本构件交互协议的交

8、互过程的控制流和数据流的复杂性质。论文证明了在输入有界条件下，基本构件交互协议的LTL-FO属性验证问题是可判定的，并给出了针对LTL-FO属性的判定算法，实现了对应的模型检查器MC4CIP，实验表明MC4CIP可以在各类场景下进行有效的验证。(4)针对嵌入式软件构件交互协议的性质验证问题，论文在FO-LTL的基础上提出了带有承诺理论扩展的线性一阶逻辑（First-OrderLinearTemporalLogicwithCTCommitmentTheor