在最新版的软件评测师教程中，可信软件验证技术作为新技术进行了新增，在考试大纲中作为上午场考试的范围。为了应对今后的考试，我们把相应的知识点进行一个总结学习，并在文章末尾配备对应的习题。
一、可信软件的概念
（1）美国科学与技术委员会NSTC给出定义：一个系统是高可信的，即使在系统存在错误、环境存在故障或者系统遭到破坏性攻击的情况下，设计者、实现者和用户都能极大程度上保证该系统不会失效或表现不好。
（2）美国国家研究委员会NRC给出定义：一个系统即使在运行环境发生崩溃、操作人员出现操作错误、系统遭到恶意攻击、系统存在设计和实现错误的情况下，也能够按照预期的方式运行，那么该系统是可信的。
（3）国家自然科学基金委给出定义：是指软件系统的动态行为及其结果总是符合人们预期，并在受到干扰时仍能提供连续服务的软件，这里的“干扰”包括操作错误、环境影响和外部攻击等。
二、软件可信评估与传统的软件质量测量的区别
软件可信性是软件质量的一种特殊表现形式，是传统软件质量概念在互联网时代的延伸。因此，可信评估本质上也是软件质量的测量，但是它与传统的软件质量测量又有所不同。
（1）软件在运行时可能会受到木马、病毒、窃听等外界的恶意攻击，传统的仅考虑自身系统质量的质量测量已难以适用，需要考虑软件实际运行时的使用质量。
（2）传统的质量测量通常针对具体的质量属性，如正确性、容错性、易安装性等，较少考虑不同质量属性的综合。而可信性是软件系统的可用性、可靠性、安全性、正确性、可预测性等诸多属性在使用层面的综合反映，因此可信评估关注的是不同质量属性的综合。
（3）传统软件质量测量的客观性较高，而可信评估则是主观与客观的结合。可信本身是一个复杂的概念，不同的研究学者对其有不同的认识。软件可信性既有客观的因素，又有主观的成分，不同应用领域(甚至同一领域)、不同任务需求、不同人员在不同时间段对可信性的定义和标准都可能不一样。而且使用质量的度量依赖于进行测量的环境，随着评估人的不同而发生变化，相对而言，可信评估在较大程度上涉及用户个性化的体验和评价。
三、可信软件的验证技术-形式化建模与方法
形式化模型来源于原始需求的逐步演化求精，因此不可避免地存在各种各样的错误，例如语法错误、功能缺失，功能之间存在逻辑上的不一致等。为了保证形式化模型能完整无缺且正确地描述人们对软件的真实期望，需要有一定的方法对形式化模型进行分析与验证。
形式化系统分析与验证分为以下几个步骤:
（1）通过数据流描述、变量关系描述和软件体系结构描述等图形符号，从形式化需求模型中抽取不同形态的分析模型。
（2）根据软件的特点划分为不同分析目标，为每个验证分析目标定义出相应技术。
（3）针对建立的性质集合，采用模型检测的方法自动地发现漏洞与验证软件是否满足高安全可靠性需求。
（4）自动生成测试用例，基于系统模型及需求自动生成关于软件实现的测试用例集，提高系统测试的效率和错误发现能力。
（5）将形式化模型进行仿真。仿真主要用于检测模型中人们所关心的系统行为在执行时是否存在错误，是一种类似于“运行”系统来暴露错误和缺陷的分析方法。
相对于测试，形式化验证的方法就是借助数学的思想和方法对软件程序是否满足性质归约进行证明或者证伪。因其高度严谨的特点，形式化验证成为保障软件正确性的关键方法。目前最主流的形式化验证技术有如下两种：
（1）定理证明：把软件系统是否满足性质归约的问题转化为定理的形式，然后通过数学逻辑公式和推导演绎规则进行验证。尽管是众多方法中最准确的，但它是经验主义导向的，不仅要求实施人员具备专业的逻辑表达能力和数学演绎推演能力，还需要有一定的行业知识背景。另外一个很大的缺陷是其自动化程度低，需要人工干预，存在因引入人为因素而影响其验证正确性的隐患。虽然它很适合用于层次化的开发过程和程序功能描述，但是对于时态性质方面的推理证明显得略有不足。
（2）模型检查：主要思想是用一个模型转换图对软件系统的程序状态和状态之间的迁移关系进行形象建模，用时态逻辑公式对性质归约进行刻画，然后来验证性质归约是否被满足。线性时态逻辑LTL是目前广泛应用的时态性质的规范语言。与定理证明不同的是，模型检查是高度自动化的，而且能在性质违反时给出反例。
四、可信软件验证工具
由于软件领域的发展，特别是可信软件的发展，形式化验证技术也越来越受到重视，而使用形式化验证的工具可以使得验证工作快捷高效。主要包括以下三种形式化验证工具：
（1）Spin：是一款开源的形式化软件验证工具，用来分析和验证并发系统逻辑是否一致的辅助验证器，它主要是针对软件检测，而不是验证硬件是否能高效运行。
（2）NuSMV：该工具被设计成一个开放的验证工具，不仅开源而且很容易修改、定制和扩展。系统结构是以模块的形式构建和组织的，每一个模块执行一套功能，并且可以通过精确定义的接口和别的模块通信。
（3）Atelier-B：是一种用于描述、设计计算机软件的方法，支持在从抽象到具体的各个层面上对软件规范进行描述，覆盖了从规范说明到代码生成的整个软件开发周期。
基于以上的知识点，结合可能出现的题目考察形式，给大家出几道练习题加以巩固。
【习题1】以下属于可信软件验证常用的工具的是（ ）
①Hadoop
②Spin
③NuSMV
④LoadRunner
⑤Atelier-B
⑥Jmeter
A、①②③④
B、①②③④⑤⑥
C、②③⑤
D、②④⑤⑥
解析：本题考查可信软件验证常用工具。
②③⑤属于可信软件验证常用工具，Hadoop属于大数据测试工具，LoadRunner和Jmeter是性能自动化测试工具。
故正确答案为：C
【习题2】在以下新技术当中，（ ）是指软件系统的动态行为及其结果总是符合人们预期，并在受到干扰时仍能提供连续服务的软件，这里的“干扰”包括操作错误、环境影响和外部攻击等。
A、移动应用软件
B、物联网软件
C、大数据系统
D、可信软件
解析：本题考查对新技术的认识。
题干描述的是国家自然科学基金委给可信软件的明确定义。
故正确答案为：D
作者唯一官方个人微信公众号（昊洋与你一起成长）：HYJY20180101
写于2021年8月30日
作者：昊洋讲师
版权所有，侵权必究
