嵌入式软件可信性建模与验证技术的研究及其应用

发布时间：2018-03-19 10:35

本文选题：嵌入式软件　切入点：可信性　出处：《南京航空航天大学》2016年博士论文　论文类型：学位论文

【摘要】：嵌入式软件在关键领域的广泛应用使其对可信性的需求远远高于一般软件。由于嵌入式软件在体系架构、资源限制、应用环境等方面的特殊性,以及近年来复杂化、规模化与开放化的发展趋势,保障和评估嵌入式软件的可信性已成为国内外越来越关注的研究热点之一。在嵌入式软件开发早期对其可信性进行分析、验证与评估,能够减少潜在的软件缺陷,从而降低后期测试与维护的成本。本文立足于可信嵌入式软件的建模与验证问题,旨在建立基于模型驱动的嵌入式软件建模与验证集成框架;采用Z语言为该框架提供形式化语义,针对嵌入式软件可信属性开展建模、验证与评估技术的研究;设计并实现了相应的原型系统,在嵌入式软件实例上进行应用研究。论文研究工作的主要创新性成果如下:(1)根据嵌入式软件的可信需求,提出了一种嵌入式软件形式化模型Z-MARTE,包括Z-MARTE时间模型、结构模型与行为模型。与现有模型相比,Z-MARTE是一种静态结构与动态行为的综合模型,能够同时描述嵌入式软件功能结构、时序行为以及可信约束。在Z-MARTE模型中引入了可信构造型的概念,通过对可信构造型的声明与约束,能够描述包括数据约束与时间约束在内的各类可信约束,为嵌入式软件可信性的验证与评估提供形式化语义基础。(2)为了对Z-MARTE模型描述的可信约束进行自动验证,提出了一种基于模型检测技术的嵌入式软件可信验证方法。首先,给出了有限域上Z-MARTE行为模型的语义解释,为模型检测方法提供了行为语义基础;其次,扩展了CTL的语法与语义,定义了一种描述嵌入式软件可信性质的时序逻辑公式ZMTL;最后,设计了有限域Z-MARTE行为模型上的模型检测算法FZMCA,能够在有限域内对Z-MARTE模型中的实时性、安全性等可信性质进行自动验证。(3)为了对Z-MARTE模型进行进一步的评估与分析,提出了一种嵌入式软件风险评估方法RAMES。首先,对Z-MARTE结构模型进行精化与扩展,提出了一种嵌入式软件对象-消息-角色模型OMR;在此基础上提出了风险分析算法RAOMR,以OMR模型中的嵌入式软件对象为评估单位,以对象间的通信行为与软件安全约束为评估依据进行风险评估,并进行了算法复杂度分析与实例研究。RAMES方法遵循ISO 31000标准的风险管理过程,其评估结果能够指导嵌入式软件设计模型中安全资源的合理分配。(4)在上述研究成果的基础上,建立了一个嵌入式软件可信性建模与验证集成框架,设计并初步实现了一个原型系统。在Eclipse平台上初步实现了一个基于XSLT转换技术的模型转换工具ZMT,将半形式化建模环境Open Embe DD与形式化建模环境CZT进行了集成;在VC 6.0平台上,对Z-MARTE模型解析模块、Z-MARTE行为模型生成模块与FZMCA模型检测模块进行了研究与实现;最后,对原型系统的应用技术进行了研究。
[Abstract]:The widespread application of embedded software in key fields makes its demand for credibility much higher than that of general software. Due to the particularity of embedded software in architecture, resource limitation, application environment and so on, it is complicated in recent years. With the development of scale and openness, ensuring and evaluating the credibility of embedded software has become one of the research hotspots at home and abroad. In the early stage of embedded software development, the credibility of embedded software is analyzed, verified and evaluated. It can reduce the potential software defects and reduce the cost of later testing and maintenance. Based on the modeling and verification of trusted embedded software, this paper aims to build an integrated framework for modeling and verification of embedded software based on model-driven. Z language is used to provide formal semantics for the framework, modeling, verification and evaluation techniques for trusted attributes of embedded software are studied, and the corresponding prototype system is designed and implemented. The main innovative achievements of this paper are as follows: 1) according to the trusted requirement of embedded software, a formalized model of embedded software Z-MARTEincluding Z-MARTE time model is proposed. Compared with the existing models, Z-MARTE is a comprehensive model of static structure and dynamic behavior, which can describe the functional structure of embedded software at the same time. The concept of trusted constructive type is introduced into Z-MARTE model. By declaring and constraining trusted stereotype, we can describe all kinds of trusted constraints, including data constraint and time constraint. This paper provides a formal semantic basis for credibility verification and evaluation of embedded software. In order to automatically validate the trusted constraints described by Z-MARTE model, a method of trusted verification based on model checking technology is proposed. In this paper, the semantic interpretation of Z-MARTE behavior model over finite field is given, which provides the basis of behavioral semantics for model checking. Secondly, the syntax and semantics of CTL are extended to define a temporal logic formula that describes the trusted properties of embedded software. In order to evaluate and analyze the Z-MARTE model, a model detection algorithm named FZMCA based on the behavior model of Z-MARTE in finite domain is designed, which can automatically verify the real-time, security and other trusted properties of the Z-MARTE model in the finite domain. In this paper, a risk assessment method for embedded software, Rames, is proposed. Firstly, the Z-MARTE structure model is refined and extended. In this paper, an embedded software object-message role model (OMRs) is proposed, and a risk analysis algorithm, RAOMR-based, is proposed, which takes embedded software objects in OMR model as evaluation unit. Based on the communication behavior between objects and software security constraints, the risk assessment is carried out, and the algorithm complexity analysis and an example study are given. The method follows the ISO 31000 standard risk management process. The evaluation results can guide the rational allocation of security resources in the embedded software design model. Based on the above research results, an integrated framework for credibility modeling and verification of embedded software is established. A prototype system is designed and implemented preliminarily. A model transformation tool based on XSLT transformation technology is implemented on Eclipse platform. The semi-formal modeling environment Open Embe DD is integrated with formal modeling environment CZT. The Z-MARTE behavior model generation module and the FZMCA model detection module are studied and implemented. Finally, the application technology of the prototype system is studied.
【学位授予单位】：南京航空航天大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP311.5

【相似文献】