可信软件非功能需求形式化表示与可满足分析

可信软件的可信性由其功能需求和非功能需求共同来体现,其中,非功能需求的实现是可信软件获得用户对其行为实现预期目标能力的信任程度的客观依据.针对可信软件的重要性以及对可信软件的迫切需求,在可信软件的早期需求工程阶段,提出可信软件非功能需求驱动的过程策略选取方法.首先,对可信软件需求进行定义,提出由功能需求和非功能需求中的可信关注点构成可信需求,非可信关注点的非功能需求则定义为软目标,用于表达质量需求,基于模糊集合论和信息熵对可信软件非功能需求进行排序并获取可信关注点和软目标.在此基础上,提出可信软件非功能需求驱动的过程策略选取方法.传统的软件早期需求工程阶段的目标是为了获取满足需求的技术及设计决策,与此不同,本文对可信软件非功能需求进行分析的目标是获取过程策略,从过程角度解决可信软件生产问题.由于非功能需求间复杂的相关关系,尤其是因为存在冲突关系,故提出了基于可满足性问题求解方法推理过程策略的方法,选取满足可信软件非功能需求的过程策略.最后,通过第三方可信认证中心软件的案例,说明所提出方法的可行性.

Formal Analysis to Non-Functional Requirements of Trustworthy Software

The trustworthiness of software is determined by both its functional requirements and non-functional requirements. Especially, the non-functional requirements are the determinants of the trustworthy software that show how it achieves the users' desired goals. Considering the importance of trustworthy software and the urgent needs for it, an approach to obtaining process strategies for trustworthy software in the early phase of requirements engineering is proposed. Firstly, the definition of trustworthy software requirements is defined as the combination of the trustworthiness requirements and the quality requirements. Trustworthiness requirements are defined as both functional requirements and trustworthiness concerns. Quality requirements are defined as soft goals. Then, based on fuzzy set theory and information entropy, acquisition method of trustworthiness concerns and soft goals is proposed. On this basis, process strategies for obtaining framework are proposed. Unlike the traditional early-phase requirements engineering which focuses on technical and design decisions, the aim of this study is to make process decisions to support trustworthy software development. In addition, to address the conflict relationships of the non-functional requirements, a reasoning method is developed for solving satisfiability problems of non-functional requirements in trustworthy software. Finally, through analyzing a trustworthy third-party certificate authority software case, feasibility of the proposed approach is described.