译 者 序 21世纪是信息时代，尤其是计算机时代，也可以讲21世纪是嵌入式系统时代。从复杂的航天系统到简单的遥控器，无不与嵌入式系统相关。嵌入式系统已经与我们的日常生活密切相关，例如，移动电话、PDA、电子阅读器、各种家电、汽车、门禁系统、各种IC卡等等，可以讲，如果现在离开了嵌入式系统，我们的日常生活工作将无法正常进行。嵌入式计算就是在这种背景下提出来的，这也足以说明嵌入式系统的普及程度和重要性。 从安全可靠的角度来讲，嵌入式系统可以分为安全关键的(safety-critical)和非(或一般)安全关键的。属于安全关键的嵌入式系统有车辆、飞行、核电厂和医疗设备等方面的控制系统。属于非(或一般)安全关键的嵌入式系统有移动电话、HDTV、家电控制器等。不管嵌入式系统是否为安全关键的，可靠性都很重要。安全关键的系统出现问题可能意味着巨大的生命财产损失，而对于非(或一般)安全关键的嵌入式系统来说，出现问题时即便不会造成任何生命财产损失，也意味着对用户使用信心的打击，而这将直接关系到相关产品的市场前景。那么如何保证嵌入式系统和软件的可靠性呢？本书正是为此而编写。本书系统地讲述了嵌入式系统设计流程中各个阶段的验证问题。当然，根据嵌入式系统不同的安全需求，考虑到成本因素，在验证上可以区分对待。相比一般系统而言，对于安全关键的系统必须进行更加严格的验证。 本书的显著特征是针对嵌入式系统和软件这个特定的领域，从不同的层面系统地讨论了各种验证方法。本书具有的第二个特点是，与一般讲理论的书不同，本书在讲述过程中紧密结合具体示例(如空中交通管制系统和汽车控制系统)和标准案例(西门子基准测试套件中的代码段)。此外，本书还有针对性地给出了少而精的习题，为巩固相关知识和激发读者思考提供了良好的题材。 本书由国防科学技术大学的田尊华翻译，由肖国尊负责监督本书的翻译质量和进度。鉴于译者水平有限，时间仓促，不足和疏漏之处在所难免，敬请广大读者提供反馈意见。读者可以将意见发送到wkservice@vip.163.com，我们会仔细查阅读者发来的每一封邮件，以求进一步提高今后译著的质量。 译者 2010年3月 前 言 本书针对的主要是嵌入式软件和系统的验证问题。有很多关于该主题的书籍，用适当的搜索术语在Web上搜索一下，就可以证明这一点。既然如此，为什么还要编写本书呢？ 可以从几个方面来回答这个问题。首先，也是最直接的回答就是，现有的有关书籍大多都是关于嵌入式系统编程或协同设计方面的。在这些书籍中，验证通常作为附带内容在最后才进行讨论。在本书中，我们将验证看作设计过程中的首要内容，并将验证过程与设计过程本身结合在一起。 本书的重点在于验证，但这里的验证是着眼于嵌入式软件和系统的。本书涉及的方法(测试/模型校验)还可以从完全通用的角度来讨论，只关注技术，而不考虑如何将这些技术用于系统设计过程。但是，我们没有这样做。虽然本书的重点在于验证方法，但是我们仍然清楚地讲述了如何将它们用于系统设计。作为一个示例，我们分别两次以不同的方式提出并讨论了模型校验方法，即分别在系统模型的层面上(第2章)和在系统实现的层面上(第5章)。 最后，本书的重点基于嵌入式软件和系统，但并不限于功能验证。我们至少还讨论了另外两个方面的内容，即性能和通信行为调试。因此，本书包含了很难在一本书中找到的分析方法，包括测试(非形式化验证)、模型校验(形式化验证)、最差情况执行时间分析(程序性能静态分析)、可调度性分析(系统级性能分析)等等，它们有机地交叉融合在一起，以便帮助您实现可靠的嵌入式系统设计。 本书的第1章对嵌入式系统验证中的问题进行了一般性介绍，并从整体的角度对功能和性能验证的差异进行了讨论。 第2章讨论了模型级(level of model)验证。我们从对系统结构和行为的一般性讨论开始，然后逐步讲解类似有限状态机(Finite-State-Machine，FSM)和消息顺序图(Message Sequence Chart，MSC)这样的具体行为建模概念，并对这些模型的仿真(simulation)、测试和形式化验证进行了讨论。我们讨论了基于模型的测试，在这种测试中使用由模型生成的测试用例(test case)对系统实现进行试验。另外还介绍了属性校核(property verification)和常用的模型校验方法，并在该章最后对SPIN和SMV这样的实用验证工具进行了很好的讨论。由此可见，该章的内容对应于模型级调试(model-level debugging)。 第3章讨论了解决嵌入式系统组件之间的通信不兼容性的问题。我们讨论了解决这类不兼容问题的不同策略，如用合适的接口增强组件，或构建一个集中通信协议转换器。由此可见，该章内容对应于通信调试(communication debugging)的内容。 第4章讨论了系统级性能验证。我们首先介绍了软件时间分析，并着重讨论了最差情况执行时间(Worst-Case Execution Time，WCET)分析。接着对程序执行过程中不同干扰导致的时耗估计进行了讨论，其中干扰可能来自外部环境，也可能来自相同或不同处理单元上执行的其他程序。另外讲解了用于估计这些干扰导致的时耗的合适分析方法。然后，我们讨论了通过系统级支持来解决执行时间不可预测性的机制。尤其是，描述了编译器控制的存储器或中间变量存储器。该章最后还讨论了新兴应用程序中的时间可预测性问题。由此可见，该章的内容对应于性能调试(performance debugging)。 第5章讨论了嵌入式软件的功能调试。我们对形式化和非形式化方法都进行了讨论，并且对测试和形式化校验的讨论所占的比重相近。该章的前半部分讲解了构建在测试或动态分析之上的验证方法进行了讨论，后半部分则重点讨论了形式化校验，尤其是软件模型校验。该章最后还讨论了形式化校验与测试的结合。由此可见，该章的内容对应于软件调试(software debugging)。 除了在第2章和第5章中有一些调试/验证方法是共同的之外，您可以单独阅读这些章节。但是，关于该主题的大学高年级或研究生课程可以按顺序阅读这些章节。