ACM

ACM通信

首页 / 杂志存档 / 2006年12月(第49卷第12期) / 正式验证和软件产品线 /全文

软件产品线工程

正式验证和软件产品线

岸信介、野田纳津子著
ACM通讯，2006年12月，第49卷第12期，73-77页
10.1145/1183236.1183270
评论

认为: 打印手机应用程序 ACM数字图书馆全文(PDF) 分享: 通过电子邮件发送在reddit分享在StumbleUpon分享分享到黑客新闻在推特上分享在Facebook上分享

嵌入式计算技术的进步使得社会极其依赖于汽车、移动电话、家用电子产品和许多其他应用中的嵌入式软件。因此，嵌入式软件的可靠性在日常生活的许多方面都至关重要。过去，嵌入式软件的开发一直是以实现为中心的;然而，由于软件的规模和复杂性的增加以及开发时间的减少，使用传统技术很难生产出可靠的软件。因此，嵌入式软件的质量成为一个值得关注的问题。为了解决这一问题，各种软件工程技术，如分析/设计方法和重用技术被引入。产品线工程是基于这些结果的最先进的软件实践之一[2］．

预计除了这些工程方法之外，还将引入诸如正式验证等科学方法。与常规测试不同的是，在常规测试中，我们只运行有限数量的测试用例，这种技术如果成功，将彻底验证目标系统的属性。正式的验证有很长的历史，据报道在许多情况下都是成功的。然而，这些案例大多属于硬件领域或关键软件领域，如军事和航空电子。此外，正式验证应用于民用行业的嵌入式软件开发，如汽车、通信和消费电子迄今为止受到了限制。其中一个主要原因是这些技术需要大量的时间和人力资源。在此背景下，我们研究了形式验证技术在软件产品线开发环境中的应用[6，7］．这是因为民用行业的大多数嵌入式系统都是作为产品线开发的，我们可以期望通过重复使用验证方案来降低成本。已提出重用测试计划[9];在本文中，我们将其扩展到形式验证。

回到顶部

轻量级软件设计验证

在这种方法中，我们将模型检查技术应用于设计验证。模型检查技术是一种形式化的验证技术，在这种技术中，我们将目标系统描述为有限状态模型，并提供一些逻辑属性，模型检查器自动检查给定的属性是否有效[10］．由于嵌入式软件必须对其环境中发生的每一个可能的事件组合和序列作出适当的反应，因此有必要详尽地检查其行为。模型检查技术适用于这种类型的验证[4，8］．此外，我们专注于设计验证而不是代码验证;这是因为设计阶段嵌入了许多bug，在编码之前验证设计是很重要的。

将这些技术应用于设计验证的常规方法如下所述。首先，将目标设计转化为有限状态模型(目标模型);进一步，将目标的环境表示为有限状态模型(环境模型)。环境模型被配置为向目标模型发送可能的事件序列和组合。然后，将应用模型检查器应用到目标模型和环境模型以及属性(表示为时间逻辑公式)，以验证这些属性的有效性。一个包含目标和环境模型和属性的集合被称为验证模型。应当指出，环境是指核查目标周围的环境;它可能是实际的物理环境、传感器或其他软件模块。

民用行业的嵌入式系统大部分是作为产品线开发的;通过对验证方案的重用，我们可以期望降低成本。

我们使用UML来定义目标模型和环境模型。这些模型中包含的每个类都有定义其行为的状态模型。在这里，我们将环境模型中的类称为参与者类。图1展示了一个例子(汽车音响系统)。目标模型由两个类组成:ev -hdlr(事件处理程序)和CD- ctrl (CD控制器)，而环境模型由三个参与者类组成:两个button(按钮)和CD (CD驱动器)。在这个例子中，我们验证了以下属性:如果按钮1被释放，CD驱动器将被关闭。

在我们的设计验证中，我们使用测试场景，因为这是定义验证项的典型方法[7］．在这里，目标系统的测试场景被定义为三元组(我, {年代}，F), {年代}表示一组将被转换的事件序列T初始状态我进入最终状态F．我们开发了一个环境模型，用于发送包含在{年代}T并验证以下属性P:如果T的我接收包含在{年代}，它最终落入F．在常规的测试中，很难检查{中包含的每一个可能的序列年代}，因为可能的序列的数量通常很大。然而，在模型检查中，如果成功，我们可以针对每个可能的事件序列验证属性。例如,在图1，每个按钮的状态模型生成定义为状态机的任意长度的事件序列，目标模型从两个按钮接收事件的顺序可以被打乱。

应用模型检查技术的一个问题是状态爆炸(对于大型模型，状态空间太大而无法处理)。虽然我们验证过相对较小的软件(3K到15K行C代码)，但我们也遇到过这个问题。在这种情况下，我们使用常规的技术，如将系统划分为子系统或手工抽象设计。

回到顶部

验证通过重用

在这里，我们将考察之前在产品线开发环境中描述的设计验证的应用。在应用工程阶段，我们通过选择所需的特性来为产品设计。虽然这个过程是系统的，但开发设计的正确性不能得到保证，因为我们不能在领域工程阶段验证每一个特征组合，而设计应该在每次导出时都进行验证。如果我们在验证上花费了大量的时间，产品的交付将会延迟。我们的目标是加快这一进程。为此目的，我们检查了验证方案在整个产品线开发中的重用。这一概念是根据以下观察得出的。尽管每个产品可能表现出不同的行为，但我们可以预期一系列产品将表现出相似的行为。这意味着每个产品的验证模型也是相似的;因此，我们可以在整个产品线开发中重用验证模型。

为了在产品线开发中重用验证模型，我们在模型中定义了变异点，每个变异点的变异点，以及特性和变异点之间的联系。在产品线领域中，一种使用UML的技术已经被提出，它通过将特定的构造型(例如“可选的”和“可选的”)附加到类和关联中来表示变异点和变体[3.］．我们可以使用类似的技术来定义环境模型中的可变点，因为我们使用UML来定义环境模型。每个产品可能有不同的参与者，每个参与者可能有不同类型的事件，并生成不同的事件序列模式;因此，每个产品的环境模型可能是不同的。我们检查了这些环境模型之间的共性和可变性，并通过使用UML技术定义了一个可重用的模型。图2展示了一个可重用验证模型的示例。在这种情况下，目标模型包括一个可选类和一个可选类，它们可能会被使用，也可能不会被使用，这取决于产品。类似地，环境模型有两个可选的参与者。对于一个替代类，定义了多个显示不同行为的变体类。

我们已经为前面描述的设计验证开发了一个支持工具(参见图3)．该系统是在Eclipse平台上开发的(参见www.eclipse.org)，并使用了SPIN模型检查器[4］．使用Modeler，用户可以定义UML模型(目标和环境模型)，描述产品线特征的特征模型[5]，以及它们之间的验证项目和链接。验证项是一组属性和其他必要信息，稍后将对此进行描述。通过指定产品，Link Manager派生验证模型和必要的验证项。Translator将模型转换为SPIN (Promela)的输入语言，SPIN验证验证项中定义的属性。由于每个验证项的初始状态、属性的初始值和转换规则(例如，如何处理状态模型中未定义的事件)可能是不同的，因此它包含这个信息以及SPIN选项。当验证失败时，SPIN会显示一个反例(违反给定属性的执行跟踪)。由于反例是基于Promela的，Viewer以UML序列图的形式显示它。

产品线开发的重要目标之一是及时交付产品。为了实现这一目标，我们必须减少产品的推导和验证所需的时间。

我们已经根据一家公司提供的实际测试场景评估了我们的方法。在这个评估中，我们可以验证大约70%的必要测试场景。我们无法测试其他的30%，因为它们包含了一些方面，比如模型检查器无法有效处理的实时约束。进一步，我们可以通过组合具有相同值的场景来减少大约10%的测试场景我而且F．除了我，大约30%的测试场景是相同的，我们可以为这些测试场景重用相同的状态模型，因为我们的工具可以更改我为每个验证项目。通过从产品家族中选择三个产品，我们已经验证了测试场景的可重用性，并发现70%的测试场景可以共享或重用。考虑到目标模型可以使用可重用的验证模型进行系统验证，结果似乎是积极的。

回到顶部

验证重用

我们在应用工程阶段引入了形式化验证的应用。在这里，我们简要地解释了形式化验证在领域工程阶段的应用。在此阶段，我们开发可被许多产品使用的核心资产。因此，必须对这些资产的每一种可能使用情况进行验证。在这里，情况不仅意味着组件的使用，如参数值和调用序列，而且还意味着组件在什么情况下使用，如组件的相对优先级和共享资源的使用情况。在实际情况下，把所有可能的情况都进行核实是不合理的，因为必须考虑大量的情况[1，10］．因此，我们必须制定一项策略来减少这种情况的数量。

为了测试核心资产，我们提出了一种技术，具体假设将使用该核心资产的潜在产品，并从这些产品中测试它[9］．我们在正式的验证中应用了这种技术。在我们的方案中，核心资产被表示为目标模型，并定义了环境模型来表示核心资产在潜在产品中的用途。在图2，让我们假设我们想要验证EV-hdlr-A作为核心资产。EV-hdlr-A的环境模型如下:首先，与测试一样，确定潜在的用途(产品)。在我们的方法中，这对应于模型上的约束的添加，例如变量的选择。其次，标识与EV-hdlr-A直接交互的类。第三，通过确定关联的多重性的具体数量来定义实例结构。最后，研究了间接影响EV-hdlr-A行为的类;这些类与EV-hdlr-A共享资源。我们认为最后一步很重要，因为仅仅通过考虑直接交互是很难验证设计的。10］．

回到顶部