下载掌阅APP，畅读海量书库
立即打开
严密系统设计方法 [1] 将系统设计活动视为一个从需求到形式化模型再到可执行代码的转换过程，其中，形式化模型不仅包括实现系统功能的应用软件模型，也包括描述系统运行平台和外界环境的抽象模型，系统形式化模型到可执行代码的转换采用了基于模型的代码自动生成和优化技术。
严密系统设计方法是一个可迭代、可解释、可回溯的设计过程。 可迭代（iterative） 是指这个过程包括一系列具有严格定义的步骤，并且明确了： ① 哪些环节需要设计人员发挥创造性，解决需求分析和设计方案选择等问题； ② 哪些环节可以借助软件工具，自动化完成烦琐且容易出错的设计任务。 可解释（accountable） 是指在所有待分析的系统属性中，系统设计人员不仅能解释哪些属性能够得到满足，也能解释哪些属性无法得到满足。 可回溯（traceable） 是指如果一个系统属性在某个设计阶段中得到满足，那么该属性应当在所有后续设计阶段中均得到满足。可回溯性可以通过采用具有 属性保持（property preserving） 特性的模型转换方法得到保证。
严密系统设计方法是一种基于模型的设计方法。该方法采用一种统一且具有严格形式化语义的建模语言对应用软件及其运行平台进行建模，以确保不同设计阶段的模型（如需求模型、应用软件模型、系统抽象模型和系统实现模型等）满足语义一致性。在统一的模型语义基础上，该方法通过模型转换实现可执行代码的自动生成，并且通过证明模型转换的语义一致性来确保代码生成过程的正确性。
传统的系统设计方法（如“V-模型”方法）采用先构造、后验证的方式来确保系统的正确性。然而，对于大规模复杂系统而言，这种“后验式”的验证技术受限于较高的计算复杂度，在实际应用中往往不可行。为克服传统系统设计方法所面临的技术局限性，严密系统设计方法遵循 “构造即正确”（correct by construction） 的设计原则，通过组件复用和体系架构来确保模型的正确性，通过模型驱动的代码生成来确保系统实现的正确性，从而避免对“后验式”形式化验证的依赖。
在工业界的设计实践中，严密系统设计方法的思想体现在以下两类系统的设计中：一类是 硬实时嵌入式系统（hard realtime embedded system） 的设计，如飞机、汽车、核电和医疗等设备的嵌入式控制系统；另一类是 大规模集成电路（Very Large Scale Integration，VLSI） 等硬件系统的设计。下面阐述这两类系统设计技术的主要特点及其成功应用的主要原因。
（1）硬实时嵌入式系统设计 ：这类方法通常采用 领域特定语言（Domain Specific Language，DSL） 进行系统设计和相关的正确性分析验证。例如， 同步编程语言（synchronous programming language） 广泛应用于 同步反应式系统（synchronous reactive system） 的设计开发 [2] 。同步程序是由多个强同步组件组成的组件网络，组件网络的执行过程是由一系列不可中断的计算步骤组成的序列。该序列定义了逻辑时间的概念，并且在任一逻辑时刻，网络中的每个组件均同步执行一个计算步骤。通常，同步程序都是在单核处理器上实现的。如果所有计算步骤的最坏情况执行时间小于规定的响应时间，那么我们认为该同步程序满足实时性要求。此外，对于 异步系统（asynchronous system） 而言，相应的设计技术主要采用由ADA标准 [3] 定义的设计流程，并基于专用的多任务运行环境，以事件驱动的方式进行系统实现。固定的优先级调度策略可用于实现多个组件之间的资源共享。对于已知时间周期和开销的组件，调度理论可用于预测组件的计算响应时间。最后， 时间触发技术（time-triggered technique） 主要在专用平台上使用特定的编程模型来确保时序属性的“构造即正确” [4] 。
（2）大规模集成电路系统设计 ：相关的设计技术遵循严密系统设计流程，能够在功能完备且定义良好的硬件抽象层的基础上，实现从由 硬件描述语言（Hardware Description Language，HDL） 表示的结构化组件模型到实际可执行代码的自动转换。由于这类硬件系统往往使用数量有限且定义明确的同步组件，其计算模型的同构性大大简化了组件交互的分析。系统模型的正确性可以通过形式化验证技术来保证，而基于模型的代码自动生成技术能够确保可执行代码的正确性。需要指出的是，基于符号化布尔函数表示形式（如二元决策图）的高效形式化验证算法是大规模集成电路设计技术能够成功应用的关键所在 [5] 。
严密系统设计方法能够成功应用于上述两类系统的主要原因在于： ① 具有语义连贯且可回溯的设计流程，以及相应的自动化辅助设计工具支持； ② 采用体系架构和形式化方法实现“构造即正确”，并通过相关的行业规范进行标准化。然而，这些方法在复杂异构的计算系统（如信息物理系统）设计中的应用遇到一些阻碍，如缺乏通用的组件模型、难以刻画计算模型的异质性、难以描述不同特征的体系架构等难题。上述案例启发了我们对严密系统设计方法的思考，严密系统设计方法应当遵循以下四项原则：关注点分离、基于组件、语义连贯以及“构造即正确”。