实时嵌入式系统模型校验技术

模型校验是最成功的需求验证工具。模型校验的基本原理如图1所示。模型校验工具的输入是系统需求或设计(称为模型)以及最终系统期望实现的特性(称为“规 范”)。如果给定的模型满足给定的规范，那么工具将输出yes，否则将生成反例。反例详细描述了模型无法满足规范的原因，通过研究反例，可以精确地定位模 型的缺陷，如此反复。该方法的原理是通过确保模型满足足够多的系统特性以增强我们对模型正确性的信心。系统需求之所以称为模型，因为这些模型表征的是需求 或设计。

图1：模型校验方法。

那 么，哪种规范化语言可以用来定义模型呢?答案当然不是唯一的，因为不同应用领域的需求(或设计)差异很大。例如，银行系统和空间系统在系统规模、结构、复 杂度、系统数据的属性及执行操作上的需求差异就很明显。相反，大多数实时嵌入式或安全临界系统都面向控制，而不是数据，这意味着这些系统的动态特性远比业 务逻辑(由系统维护的内部数据的结构及操作)重要。这些基于控制的系统可以应用于诸多领域：航天系统、航空电子、汽车系统、生物医学仪器、工业自动化及过 程控制、铁路、核电站等。甚至数字硬件系统的通信和安全协议均可视为面向控制的系统。

对于面向控制的系统，可以采用有限状态 机(FSM)定义需求和设计，这是一种得到广泛认可的抽象表示方法。当然，光靠FSM并不能对复杂的实际工业系统进行建模。我们还需要：1. 能将需求模块化并区分需求等级;2. 能合并各组成部分的需求(或设计);3. 能通过更新预先规定的变量和设备，防止可能出现的异常。

校验设计需求时，通常可以通过回答一些问题得到结果。下面给出了校验需求时最常问的一些问题：

* 设计需求是否准确地反映了用户需求?需求中的每一事项是否与用户的期望一致?需求是否包含用户所要求的全部内容?

* 设计需求是否表述清晰并无异义?是否能被用户很好地理解?

* 设计需求是否具有灵活性和可实现性?例如设计需求是否模块化并具有良好的架构，从而有助于设计和开发?

* 设计需求是否能轻松地定义验收测试示例以验证设计实现与需求的一致性。

* 设计需求是否只是概要地描述而与具体的设计、实现及技术平台等无关，从而使得设计人员和开发人员具有充分的自由度实现这些需求?

回 答这些问题当然绝非轻而易举而且也没有任何捷径可循，但如果需求成功地超越了这些条条框框，那么无疑为优良系统的设计打下了坚实基础。尽管可以利用类似 UML这样的建模工具，但仍然需要确保设计需求的质量。这个过程需要投入大量精力和时间，包括各种形式的审查，有时甚至还需要进行部分原型设计。此外，需 求设计中采用多种表示方法(如UML中的表示方法)通常又将引发其他的问题,例如:

* 设计需求需要使用哪种表示方法?

* 如何确保不同表示方法的描述的一致性?

图2：简单的双水槽泵控系统。

设计需求缺陷的成本通常很高，至少需要重设计并进行维护。错误的需求导致错误的系统行为并显著增加成本，如丧失产品的时效性和本质特征，而对于工作在实时环境下的嵌入式安全临界系统更是如此。为确保系统设计的质量，也需要考虑类似的问题。

改 进需求和设计的一条途径是利用自动化工具对需求和设计各环节的质量进行校验。那么，哪种工具最适用呢?一般而言，校验用英文描述的需求或设计极为困难。因 此，必须采用一种清晰严格且无二义的规范化语言对需求进行描述。如果这种描述需求和设计的语言具有明确的语义，那么完全可以开发出自动化工具以分析这种语 言描述的设计需求。这种采用严格语言描述需求或设计的基本思想已成为系统验证的基石。简单的系统模型实例

首 先，让我们考察一下如何利用模型校验工具验证简单的嵌入式系统特性。为此，我们采用Carnegie-Mellon大学开发的符号模型验证器 (symbolic model verifier,SMV)作为模型校验工具。当然，我们也可以采用其他的模型校验工具描述该模型。文章结束部分列出了可选的模型校验工具及获取方式。

如 图2所示，一个简单的泵控系统通过泵P将源水槽A中的水传送至接收水槽B。每个水槽都具有两级刻度线：一个用来检测水位是否为空(Empty)，而另一个 用来检测水位是否已满(Full)。如果水槽的水位既不为空也不为满，那么水槽刻度线设定为ok;换言之，即水位高于空刻度线但低于满刻度线。

最 初，两个水槽均为空。一旦水槽A的水位值为ok(从空开始)，启动泵并假定水槽B尚未为满。只要水槽A不为空且水槽B不为满，泵将持续工作。一旦水槽A为 空或水槽B为满，泵将停止工作。一旦泵启动(或停止)，系统将不会尝试停止(或