论文部分内容阅读
随着计算机技术的不断发展,软件应用领域越来越广。然而由于问题的复杂度、用户需求的多变和运行环境的动态演化等原因,规模日趋庞大的软件经常发生各种故障,软件可信性问题日益突出。为减少软件失信造成的损失,提高软件的可信性已经成为国内外的研究热点。为提高软件可信性研究人员在可信软件的基础理论模型、安全保障、测试和度量标准等方面取得了一系列研究成果,但是很少有研究将关注点放在软件生命周期上去考虑软件的可信性。针对上述现状,本文以软件体系结构和可信计算两个领域的理论为指导,从构造可信软件的角度出发,在软件生命周期的各个阶段考虑如何构造高可信软件系统,系统地研究了在自顶向下软件开发过程中构造高可信软件涉及的一些关键技术。首先在ADL中形式化地引入可信属性使得系统在总体设计阶段就有可信性的保证;其次设计一种组件可信性模型使得在详细设计阶段设计具体的组件时能保证各个组件的可信性;然后设计一种信任模型使得在实现阶段选择第三方组件时可以高效地选取到可信组件;最后设计一种自愈模型使得在运行阶段系统出现故障时可以自动恢复。本研究工作取得的创新性成果主要包括:1)针对目前ADL很少支持可信属性建模的现状,以TLA+为基础形式化地描述了如何建模可计量的可信属性,以此形式化语义为基础提出一种架构描述语言RXF-ADL并实现了相应的支撑工具RFX-TOOL,从而在系统总体设计阶段就可以对整个系统的及时性和可靠性做出预估;2)提出一种组件可信性模型,用集合论和谓词逻辑形式化地描述了组件的各种可信属性,包括可预测性、及时性和可靠性等,并设计转换规则将形式化描述的组件模型转换为扩展的时序自动机,从而在详细设计阶段可以使用UPPAAL工具对可信属性进行校验。该模型独立于现有的组件开发方法,也就是说并不限制开发人员采用何种组件技术去实现具体的组件。3)提出一种基于信任图的组件信任模型,该模型定义了简单有效的信任计算与演化规则,然后以此模型为基础实现了一种组件选取算法,从而在实现阶段可以有效地选取到可信的第三方组件;4)针对组件按信任值区间统计的管理性需求,提出一种新型B树结构:mcaB树,以mcaB树为底层索引结构可以高效的解决多类别区间统计问题。B树是解决区间统计的有效数据结构,它的查询和更新复杂度均为O(logCN)次I/O,其中N为总数据量,C为外存页大小。显然传统B树在解决类别数为K的多类别区间统计问题时查询复杂度为O(KlogCN)次I/O,而mcaB树的查询和更新复杂度都仅为O(logCN)次I/O;5)针对系统运行时组件可能出故障的问题提出一种基于切面的自愈引擎。自愈引擎由拦截器、自愈策略和注入点三部分组成,拦截器负责拦截组件抛出的异常,自愈策略选择合适的策略器修复故障,而注入点指出自愈引擎应该注入的位置。系统在集成自愈引擎后,在系统运行时如果组件出现异常,自愈引擎会自动介入处理异常从而透明地使系统恢复正常运行。