【作者】 刘峰；

【导师】 谭庆平；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2010， 博士

【摘要】 系统可信性是在正确性、可靠性、安全性、可维护性等众多概念的基础上发展起来的一个新概念。一般认为,系统具有高可信性是指系统的动态行为及其结果总是符合人们的预期,系统在受到诸如操作错误、环境变化、外部攻击等干扰时仍能成功地向用户提供连续的服务。工业界和学术界逐步认识到可信性已经成为信息系统的内在固有属性。然而,可信性不是安全性、可靠性等诸多属性的简单叠加。传统衡量系统质量的各个属性是从不同的视角定义的,它们之间存在相互关联和影响,将它们综合起来作为可信性的解释并不合理。目前,学者们仍不断尝试从各个角度、多种层次去诠释系统可信性,并以此为指导发展系统可信性增强技术。系统可信性研究范围非常广泛,涉及计算机系统的各个领域。小到简单的硬件模块,大到复杂的分布式网络系统都存在可信性问题。系统可信性研究既要对多个领域的共性问题进行理论探讨,也要针对具体应用领域的特点进行技术创新。本文在研究系统可信性一般性问题的基础上,着重对计算机算术领域混合算术加法中的可信性问题及其相应的可信性增强技术进行了研究和探索,希望对提高微处理器计算部件的设计水平有所帮助。本文在社会学、心理学等领域提出的信任模型和计算机领域现有的系统可信性模型的基础上,描述了一个通用的信任模型,并以该通用信任模型为基础,提出了一个新的系统可信性模型。本文提出的系统可信性模型总结了可信性的特点和主要研究内容,阐述了提高系统可信性的主要方法和途径。以提出的系统可信性模型为指导,本文着重研究了浮点乘加部件中混合算术加法的可信性问题,并以IBM POWER6微处理器中128位循环进位混合加法器为应用实例研究了算术加法可信性增强的关键技术,它们包括:硬件部件功能正确性分析和证明,硬件部件非功能属性(如功耗等)的评估与优化以及硬件系统高层次建模与模型转换等。针对算术加法部件的功能正确性,本文提出了基于半群理论的算术加法形式化分析和证明方法。本文首先基于半群理论和归纳法形式化地描述和证明了行波进位、超前进位、并行前缀等较基本的算术加法算法的正确性。以此为基础,本文提出了一种通用选择进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。然后,融合上述加法算法,本文提出了一种通用循环进位/并行前缀混合算术加法的系统结构,并分析和证明了该系统结构的正确性。本文的工作确保了遵从该通用循环进位/并行前缀混合加法系统结构而设计的加法器在算法层次的正确性。IBM POWER6 128位循环进位加法器是该通用系统结构的具体实例,因此其正确性也很容易得到了验证。针对算术加法部件功耗等非功能属性,本文提出了基于面向方面的硬件设计空间搜索方法,在设计早期就对硬件系统的功能和非功能属性进行分析和评估,提高了搜索满足多个约束条件的优化设计方案的效率。IBM POWER6循环进位加法器作为示例说明了该方法的有效性。此外,本文提出了基于模型驱动开发和面向服务建模的硬件高层次建模与设计方法。该方法通过提高系统设计描述的抽象层次和模型自动转换来提高系统开发的效率并增强系统设计的可信性。IBM POWER6的循环进位加法器同样作为示例验证了该方法的有效性。最后,本文还讨论了基于UML的高层次面向方面的硬件系统建模方法。更多还原

【Abstract】 System trustworthiness is novel concept based on properties such as correct-ness, reliability, safety, maintainability and so on. Traditionally, trustworthiness isdefined as the system’s behaviors and its results are always consistent with the user’sexpectations. When there are some interferences from operation errors, environmentchanges and outside attacks, the trustworthy system is required to supply servicessuccessfully and continuously.Industry and Academic begin to acknowledge that trustworthiness is a intrinsicproperty of the system, which is not a simple union of attributes such as security,reliability and so on. It is well-known that traditional quality attributes are de-fined from various perspectives, which are not orthogonal. It does not make senseto understand trustworthiness as a holistic property of the system, encompassingall of the traditional quality attributes. Right now, researchers are trying to ex-plain the concept of trustworthiness from various perspectives and develop relatedtrustworthiness improving techniques.Based on the trust models from the sociology, psychology and the existingsystem trustworthiness models from the computer science, this paper presents ageneral trust model and a novel system trustworthiness model. The characteristicsof trustworthiness and its main research contexts are concluded in the proposedsystem trustworthiness model, which also explains the trustworthiness improvementtechnologies.By the proposed system trustworthiness model, this paper focuses on the keytechniques of trustworthiness improvement on hybird arithmetic addition of ?oating-point fused multiply-add unit, including analysis and proof of the hardware func-tionality correctness, estimation and optimization of the non-functional propertiessuch as power consumption, as well as high-level hardware modeling and modeltransformation. The end-around-carry adder in IBM POWER6 microprocessor istaken as the case study in this paper.For the correctness of arithmetic addition algorithms, the semi-group basedformal analysis and proof methodology is proposed in this paper. Firstly, the cor- rectness of basic addition algorithms such as ripple carry adder, carry look-aheadadder and parallel prefix adders are proved. Then, a general architecture for the de-sign of hybrid prefix/carry-select adder is proposed. A detailed proof of this generalarchitecture is described. By the above addition algorithms, a general architecturefor the design of hybrid prefix/end-around-carry adder is developed. The details ofits correctness proof are also described. This ensures the algorithm level correctnessof the real design of end-around-carry adder followed the general architecture. Theend-around-carry adder in IBM POWER6 microprocessor is a special case of theproposed hybrid prefix/end-around-carry adder general architecture, which meansits correctness can be verified easily.For the adder’s non-functional properties ( such as power consumption ), thispaper presents an AOP-based hardware design space exploration methodology, whichdoes the analysis and estimation for the hardware system’s functionality and non-functional properties at the early stage of the design circle. This methodology ishelpful to search the optimized design under a number of constraints. The IBM’send-around-carry adder is taken as a case study to show the e?ectiveness of theproposed methodology.Furthermore, this paper also presents a MDA-based and service-oriented high-level hardware modeling and design method. By using the high-level modelingtechnology and model transformation, the e?ciency of system development and thesystem’s trustworthiness can be both improved. The IBM’s end-around-carry adderis also taken as a case study to show the e?ectiveness of the proposed methodology.At last, the paper discusses the UML-based method to model the notions of AOPfor hardware design at the high level of abstraction.更多还原