嵌入式系统验证简介.doc

PAGE 4 嵌入式系统设计的验证与调试技术 PAGE 3 第1章 嵌入式系统验证简介 1CHAPTER 1 CHAPTER 嵌入式系统验证简介 嵌入式软件和嵌入式系统已经逐步成为我们日常生活中使用计算机和计算的主导方式。计算机不再是放在桌子上的独立实体，相反，通过我们直接或间接使用的小型设备，计算机已经完全融入了我们的日常生活，这些设备包括移动电话、洗衣机、微波炉、汽车控制器和飞行控制器。实际上，嵌入式系统是如此普及，以至于今天它们可以完成大量的计算任务，从而使“嵌入式计算”成为一个新的研究领域。本书主要关注嵌入式软件和系统的验证，其目的是要开发出具有可靠功能和时间特性的嵌入式系统。 并非所有的嵌入式系统都是安全关键的。一方面，有很多安全关键的嵌入式系统，如汽车、交通(火车)控制、飞行控制、核电厂和医疗设备。另一方面，还存在更多的一般或不是那么安全关键的嵌入式系统，如移动电话、HDTV(高清晰度电视机)、家用设备(如洗衣机、微波炉和空调)控制器、智能衬衫等等。毫无疑问，不管嵌入式系统是不是安全关键的，将验证过程集成到嵌入式系统设计流程中的每个阶段都是至关重要的。当然，对于安全关键的嵌入式系统，有必要进行更加严格的验证。正因如此，所以要使用形式化分析方法，因为这样可以为系统的功能/时间特性提供数学保证，至少在设计的某些阶段需要这样。 在本书中，我们所关注的重点在于验证方法，以及如何有效地将这些方法与嵌入式系统设计过程结合起来。在深入讨论这些内容之前，首先直观地解释一下出现在验证过程中的一些通用术语，包括测试、仿真、校验和性能分析。 测试(testing)是指对于给定的系统输入，校验系统的行为是否与期望的行为一致的过程。在此，被校验的系统可以是即将运行的实际系统。但是需要注意，只对给定的输入进行校验，并非针对所有的输入。 仿真(simulation)是指基于给定的输入来运行系统。但是，仿真在以下一个或两个方面不同于实际系统的执行： 被仿真的系统可能只是实际执行系统的一个模型。这一点对于功能仿真是有益的，因为可以在建立实际系统前，检查在所选输入情况下系统模型的功能。 系统执行的平台是仿真的，它不同于实际的执行平台。这种情况对于性能仿真非常普遍。实际系统的执行平台可能根本就不存在，或者它需要通过性能仿真过程才能确定下来。典型情况下，执行平台的软件模型是可以用于性能仿真的。 形式化校核(formal verification)是指对于所有可能的输入检查系统的行为是否与期望的行为一致的过程。穷举测试是低效的，甚至是不可行的，而校核是可以通过静态分析系统模型来实现的(系统模型可以用类似有限状态机这样的结构表示)，因而可以避免这种低效。 最后，需要注意，形式化校核方法通常用于为系统功能提供严格的数学保证。但是，为了给出性能的严格保证(例如，给出特定软件执行时间的上限)，需要应用估计性能的数学分析方法。这些方法通常都冠以性能分析的名称。 为了了解将验证过程集成到嵌入式系统设计流程中的可能性和时机怎么样，可以看一下汽车行业。普遍认为，汽车电子设备具有广阔的市场，现代汽车中越来越多的功能都是由软件控制的。实际上，汽车软件上的创新可以带来新的设计，这通常也是汽车制造商他们自己认同的观点。当今有一些著名的观点可以证明在现代汽车设计中嵌入式软件/系统的重要性，如“现在生产的汽车中超过90%的创新来自于软件”。自然，由于在汽车驾驶过程中，各种汽车部件功能“正确”十分重要，因此对控制这些部件的硬件/软件的严格验证是极其关键的。换言之，集成了各种调试/验证过程、具有可靠和健壮特性的嵌入式系统设计流程是必不可少的。 为了深入理解对于汽车而言嵌入式系统验证的重要性，我们可以更进一步地研究汽车的各个组成部件，其中有些可能是由计算机控制的。大致来讲，这些部件可以分为3类，即引擎功能、驾驶室功能和娱乐功能。显然，引擎功能是最安全关键的，而与车内娱乐相关的功能是最不安全关键的。引擎功能包括像刹车和方向盘这样的关键功能；通常这些功能与硬实时约束相关。驾驶室功能包括关键程度较低(但很重要)的功能，如电动车窗和空调装置。娱乐或信息功能包括车内设备的控制，如GPS导航系统、CD播放器和车内电视，以及这些设备间的通信功能。很显然，控制引擎功能的计算部件(如刹车)需要非常严格的验证，以至于必须对这些计算部件的行为进行形式化建模和校核。对于汽车驾驶室功能，至少需要对控制驾驶室功能的计算部件进行建模和广泛的测试。对于信息功能，我们需要使用性能分析方法来保证满足必要的软实时约束。 由此可见，与我们在汽车软件这个特定领域中讨论的一样，对于复杂的嵌入式系统往往需要进行不同类型的验证。对于系统中安全关键程度较高的部件，可能需要严格的建模和形式化校核，而对于系统中安全关键程度较低的部件