下载掌阅APP，畅读海量书库
立即打开
传统的系统设计方法只是给出了系统设计过程中应当遵循的一般性原则，并没有提供一套严密的科学理论指导和自动化工具支持。一个典型代表是基于“V-模型”的系统设计方法（简称“V-模型”方法），如图1.4所示。作为“瀑布模型”的扩展，“V-模型”方法将系统开发的全生命周期过程视为一系列从需求分析、概要设计、架构设计、模块设计到代码实现、集成测试、验收测试等阶段的活动 [4] 。“V-模型”是上述系统开发过程的图形化表示。这种设计方法已经广泛应用于中小规模安全关键系统的开发中，并且写入了相关行业的标准规范，例如，道路车辆功能安全国际标准ISO26262等。
图1.4 “V-模型”系统设计方法
直观上，“V-模型”方法主要由以下两个相互补充的设计流程组成。
一个是自上而下的设计与实现流程（图1.4中“V-模型”的左半部分），该流程从需求分析开始，经过概要设计和架构设计，将系统功能需求分解为多个组件或子模块。该流程也包括组件的模块设计及其代码实现。
另一个是自下而上的验证与确认流程（图1.4中“V-模型”的右半部分），包括组件的单元测试、集成测试、系统测试和验收测试一系列活动。总的来说，“V-模型”方法提出的系统设计流程及其存在的局限性主要体现在以下三个方面。
1.需求分析
需求描述了待设计系统的整体行为和功能，通常是用自然语言表述的。然而，这些需求描述可能存在歧义、不一致或不完整。需求分析的目的是消除歧义，确保需求描述没有矛盾，不遗漏关键系统属性。对于实际的复杂系统而言，有效地使用严格的需求规范描述语言是极其困难的。需求规范必须满足以下两个基本属性。
（1）可靠性（soundness） ：给定一个需求规范，至少存在一个系统能够满足这个需求规范。换句话说，可靠性意味着需求规范不存在自相矛盾。由于逻辑规范可满足判定算法的内在复杂性，即使对于可判定的需求规范语言，可靠性检查也可能存在困难。
（2）完备性（completeness） ：需求规范需要尽可能完整地描述系统的所有可能行为。声明性语言的完整性属性尚不存在技术标准——用声明性语言描述需求规范可能是一个没有尽头的过程。
对于安全关键系统，我们通常采用时序逻辑对需求进行形式化描述，但我们仍缺乏准确的语言来描述信息安全需求（如拒绝服务工具）和服务质量需求。
2.系统建模
“V-模型”方法假设系统的设计流程是基于模型的。这就意味着系统设计者需要使用模型来描述系统行为，并且通过验证技术来确保系统模型满足其需求规范。模型在某个抽象级别上刻画系统的行为。模型应当是可信赖的，即模型所满足的任何属性也应当适用于实际系统。理想情况下，模型应该根据系统的形式化描述自动生成。目前，对于硬件系统，我们掌握了可信赖模型的自动化生成方法。对于软件系统，我们可以生成用于验证系统功能需求的模型，前提是需求是采用具有明确语义的语言所描述的。然而，对于额外的非功能需求，例如，满足最低时限和 服务质量（Quality of Service，QoS） 需求，我们还需要考虑硬件运行平台特性。即使对于非常简单的系统（如无线传感器网络的计算节点），系统模型的自动化生成仍然是一项难题，我们不仅需要理解应用软件是否满足系统的功能需求，也需要理解应用软件与底层硬件平台之间的复杂交互。
3.验证和确认
验证 的目的是对系统模型所描述的所有可能行为进行全面的遍历，以判断其是否满足给定的属性。验证能够发现系统模型存在的设计缺陷或错误（通常，这种缺陷或错误意味着实际系统可能存在安全风险），验证也能够证明系统模型的正确性（相对于给定的属性或需求）。其中， 单一验证（monolithic verification） 技术将系统模型作为一个单一整体进行验证。考虑到模型验证的计算复杂度，单一验证技术通常适用于中小型规模的系统模型和特定属性的检测，在特定条件下该技术也能够用于大规模系统模型的自动化验证，但依旧无法解决 状态空间爆炸（state space explosion） 问题。针对该问题的一个可行的技术方案是 组合验证（compositional verification） 。然而，对于基于组件的系统模型，组合验证的尝试，如“ 假设-保证 ” （assume-guarantee） 技术，同样面临着诸多挑战。其中，最主要的挑战是如何将系统层面的全局需求分解为一组关于组件的局部需求，并且使得： ① 每个局部需求都被系统的一个组件所满足； ② 所有局部需求的逻辑析取蕴含着全局需求。目前，这些问题尚未取得重大突破 [5] 。
确认（validation） 通常是通过对一个实际的系统或一个基于模拟仿真的系统模型进行测试来完成的，主要包括根据测试用例来检查系统的行为是否正常，并判断系统的输出响应是否符合需求规范。测试技术往往不追求对系统行为的全面的遍历，因此并不受到状态空间爆炸问题的困扰，但同时也无法严格证明系统满足给定的需求规范。测试技术通常是在一定的测试覆盖率标准下，计算得到系统满足给定需求规范的置信度。
虽然形式化验证和确认能够检测系统设计相对于需求规范的错误，但其应用范围仅限于那些能够被有效地形式化描述的系统需求规范。目前，这些需求主要包括应用软件功能需求以及部分 效率需求（efficiency requirements） ，如抽象系统模型上的调度策略和资源管理策略等。实际上，对于效率需求而言，一个更加有效的方法是 强制（enforcing） 而不是检测，也就是说，不是检测给定的资源参数是否满足效率需求，而是尝试确定调度策略的资源参数，以确保效率需求得到满足。后者通常可以通过合成技术 [6] 或 自适应控制（adaptive control） 技术 [7] 来实现。然而，合成技术在计算复杂度上并不比模型验证技术低。自适应控制技术主要通过实时监控系统的运行过程或状态变化进行参数值的调整，相较于合成和验证技术，其复杂度要低得多。
需要注意的是，“V-模型”方法建立在以下假设条件之上。
（1） 该方法假设在开展系统设计时所有的系统需求都是已知的，并且这些需求可以被清晰地表述、交流和理解。
（2） 该方法假设系统设计是一个从需求开始的自上而下的过程。然而，事实上大部分系统都不是从零或者草图构思开始设计的，而是通过增量式迭代修改现有系统以及复用已有组件的方式进行构建的。
（3） 该方法认为全局系统需求可以分解为系统组件的局部需求。此外，该方法还隐含地假设了一个 可组合性原则（compositionality principle） ：若能够证明系统组件相对于局部需求是正确的，那么全局系统的正确性可以从所有系统组件的正确性证明中推断得出。然而，目前我们仍然没有有效的组合验证或证明技术。
（4） 该方法主要依赖于“验证即正确”或“测试即正确”这种“后验式”的正确性验证和确认技术。对于自动驾驶等大规模复杂系统而言，现有的“后验式”验证和确认技术面临着状态空间爆炸等问题。
这些假设条件一方面刻画了“V-模型”方法的特点，另一方面也限制了其适用范围。在实际应用中，“V-模型”方法由于存在上述假设条件所带来的局限性而受到质疑。
近年来，在软件工程领域， 敏捷开发方法（agile development methodology） [8] 作为一种替代的设计方法被提出。与“V-模型”方法更注重系统设计过程的连贯性和一致性不同，该方法更强调解决方案的增量开发和团队协作，它认为软件设计和软件编码是相辅相成的，并提倡软件设计模型应当在系统开发过程中得到分享和改进。这种方法的主要价值在于它所倡导的敏捷开发理念，以及对“V-模型”方法的审视和改进，然而，它并不是一种科学的、严密的系统开发方法。