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