理论计算机科学电子笔记128（2005）127-144www.elsevier.com/locate/entcs结合Box结构开发方法和CSP进行软件开发菲利帕·J 霍普克罗夫特1英国牛津大学计算盖伊·H 布罗德富特2Verum Consultants荷兰摘要在本文中，我们结合框结构开发方法（BSDM）[6，8]和CSP [3，10]，将它们集成到工业软件开发过程中。BSDM的开发考虑到了实际软件项目，并提供了一个框架，用于开发完全可追溯到非正式需求的正式设计规范。它可以很好地集成到工业环境中，并在正在开发的实际系统和用于形式分析的抽象模型之间形成理想的桥梁。CSP通过提供形式验证的数学框架以及模型检查器FDR来补充BSDM。在本文中，我们提出了将规范从BSDM转换为CSP的通用算法，说明了如何使用FDR对其进行正式验证，并总结了一个工业案例研究。关键词：软件设计验证，CSP，FDR，箱式结构开发方法。1介绍在本文中，我们结合了两个现有的和互补的形式化方法，将它们集成到工业软件开发过程。其中第一个是盒子结构开发方法（BSDM），最初由米尔斯[6]开发，后来由其他人扩展（例如，见[8]）。第二1电子邮件：philippa. comlab.ox.ac.uk2电子邮件：guy. verum.com1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.04.008128P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127方法是进程代数CSP [3，10]，以及它的模型检查器FDR [9，2]。激励这项工作的问题域是实用软件系统的开发，其中复杂性和并发性使它们越来越不可靠，仅用传统的测试方法。多年来，许多正式的方法已经开发出来，例如[3，4，1]。然而，将它们集成到工业软件开发环境中已被证明是困难的。有很多理由，从可扩展性到教育问题，这取决于所讨论的正式方法。我们在实践中遇到的一个常见问题是，具有必要产品知识的领域专家和业务分析师通常无法获得正式验证所需的正式规范。在每个项目开始时用正式语言培训他们是不可行的。 这导致了那些对验证过程至关重要的人被排除在外。BSDM是在考虑实际软件项目的情况下开发的，它为弥合抽象形式模型和实际软件开发过程之间的差距提供了一个理想的工具。它使用一种需求分析技术，导致一个正式的规格可追溯到原来的非正式规格。然后通过一些细化步骤将此规范转换为实现。根据第二作者的行业经验，这种方法与基于序列的规范方法[7]一起很CSP通过为形式验证提供基本的数学框架，以及提供必要自动化的模型检查器FDR来补充BSDM本文的组织结构如下。在第2节中，我们对这两个正式框架进行了概述第3节和第4节描述了如何在CSP中对BSDM第5节讨论了使用FDR模型检查器进行自动分析的范围。在第6节中，我们简要概述了如何扩展我们的方法来对BSDM中使用的一些抽象技术进行建模。最后，我们提出了我们的结论，工业应用和未来的工作在第7节。2背景2.1箱形结构展开法盒结构开发方法[5，6]定义了系统的三个功能视图，形成了一个抽象层次结构，允许逐步细化P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127129和验证：黑盒是系统外部视图的无状态描述;状态盒是从黑盒派生的，并引入内部状态;而清盒视图是状态盒的实现。每个视图必须完整、一致和跟踪正确。在实践中，我们使用这种方法来根据所有系统组件的需求制定其功能行为的严格设计规范，因此目前仅限于黑盒和状态盒视图扩展这一点以包括清除框，或从状态框描述生成代码的其他方法，是未来工作的一部分黑箱黑箱规范是最抽象的观点，它定义了系统或组件的外部行为，即来自环境的输入刺激和对其环境可观察的输出响应;S和R分别表示刺激和响应的集合。黑盒的特征是黑盒函数BB：S→R，将刺激历史映射到响应，其中S是S上所有有限序列的集合。在实践中，可能有一个刺激不调用响应;为了完整性，一个特殊的响应null被添加到集合R来处理这种情况。例如，在任何刺激输入之前的系统初始状态中，没有响应可以（自发地）发生。必须包含非法的刺激序列，并将其映射到特殊值ω∈R。非法序列是扩展封闭的：非法序列的所有扩展也是非法的。黑盒是从非正式需求中发展出来的，并且要求它是完整的、一致的和跟踪正确的。在实践中，这是很难实现的，因为需求往往是不完整的，不一致的，可以运行到数百页。在[7]中，Prowell和Poore提出了基于序列的软件规范方法，用于系统地定义黑盒规范，以确保原始需求的完整性，一致性和可追溯性。 该方法涉及有序的按长度顺序枚举S中所有可能的刺激序列，从用空序列，以及从R到每一个的响应的分配。对于每个长度，排序必须完整。在这个枚举过程中，序列之间的等价可能会出现：两个序列u，v∈S是Mealy等价的，记为u<$ρMev，正好当它们的所有非空扩张都是导致同样的反应。当序列u和先前枚举的序列v之间出现这种等价时，与u相关的响应连同其与v的等价一起被记录。如果不存在这样的等价，那么u被称为不可约的。因此，集合S被划分为等价类的有限集合，定义如下：关于我 其中，对于每个序列u∈S<$，存在唯一的不可约正规130P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127形式v使得u∈[v]ρMe;这些被称为典型序列。使用[8]中的格式，该序列枚举的结果是一组枚举表，每个规范序列c对应一个枚举表，其形式如下：正则序列：c刺激响应当量迹规则非正式需求的可追溯性是通过坚持每一个设计决策来实现的，关于响应的分配和发现的等效性，都是通过明确引用相应的非正式需求（在跟踪规则列中捕获）来证明的。在这一过程中，经常出现的情况是，需要就非正式规范没有提及、含糊不清或前后不一致的问题作出选择。在这些情况下，必须与领域专家共同制定新的要求。当应用于组织良好的软件工程过程（例如，CMM 2级及以上）时，这种方法在消除需求中的模糊性和遗漏以及在整个设计阶段保持领域专家的参与方面非常有效。一旦所有序列都被分配到一个等价类，枚举过程就完成了。例3.3以表格形式说明了一个完整的枚举。强双相似的枚举规范被认为是等价的（因为它们编码相同的黑盒）。状态框状态框规范是实现的下一步。它是从一个黑盒中派生出来的，并且它们在行为上应该是等同的。状态盒引入状态变量来捕获刺激历史的独特特征，使得其行为等同于黑盒的行为。它的特征在于一个全函数SB：（Q×S）→（Q×R），其中Q、S和R分别是状态、刺激和反应的集合Q中的状态表示特征谓词，每个等价类都有一个不同的状态，在S的划分上。定义每个等价类的状态变量及其唯一实例是通过称为规范序列分析的过程实现的，并在[8]中进行了描述非正式地说，这个过程涉及到发明变量，这些变量捕获每个刺激序列的条件。定义每个变量的值的合适范围，使得变量值的组合对于每个规范序列是唯一的状态变量的引入消除了参考刺激历史的需要，并为实现目的提供了更直观的描述。一旦定义了这些变量，状态盒的构造就如下所示：P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127131直截了当。然而，在实践中，定义合适的变量（在整体设计的背景下）可能是困难的，并导致在此阶段注入错误。一个黑盒和一个状态盒分别具有函数BB：S→R和SB：（Q×S）→（Q×R），当对于S中的每个序列，它们调用相同的响应时，它们在行为上完全等价状态盒规范表示为一组表格，每个刺激s∈S对应一个表格，其中形式：刺激：s当前状态响应新状态迹规则例4.3说明了这种表示法。在一个完整的、一致的状态盒中，人们可以确定在任何给定状态下对任何刺激s∈S2.2CSP和FDR模型检查器CSP [3]是一个进程代数，用于描述相互通信或与其环境通信的并发进程。它有一个丰富的语言和语义模型的集合，用于推理流程行为。我们在这里给出一个简短的概述;更多细节请参见[10一个进程被定义为它可以与其环境一起执行的同步原子事件：a→P可以首先执行事件a，然后像进程P一样运行。我们写信？x：A→P（x）（前缀选择结构）表示愿意执行A中的任何事件，然后表现得像进程P（x）的进程。通道携带事件集：c？x→Px从通道c输入一个值x，然后像Px一样工作。CSP有以下选择算子：PQQ表示P和Q之间的外部选择;两个过程的初始事件都被分配给环境。PHQ表示P和Q之间的内部选择;过程可以像P或Q一样行动，选择是非确定性的。过程可以并行放置，在那里它们同步于（所有或特定的）公共事件或交错，在那里它们彼此独立地运行。出于本文的目的，它需要介绍CSP中最简单的语义模型，称为痕迹模型。跟踪是一系列事件（对环境可见）。对于任何过程P，迹（P）是P的所有有限迹的集合;此外，迹（P）是非空的（总是包含空迹）和前缀封闭的。一个过程Q迹精化一个过程P，记为P±TQ，恰好当Q的每一个迹也是P的一个迹时。Traces模型132P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127JJ-仅允许我们验证安全属性CSP中存在更丰富的语义模型，以捕获更广泛的属性，如非确定性和其他活性条件。当我们扩展我们的方法来处理未充分规范时，我们在第6节中参考了这些模型FDR [9，2]是一个成熟的CSP模型检查器，它提供了完全自动化的精化验证（对于所有语义模型），确定性，死锁自由和活锁自由，以及广泛的调试工具。3CSP中的黑盒建模在本节中，我们将展示如何在CSP中对黑盒进行建模，并提出一个构建黑盒的通用算法。基于序列的黑盒规范描述了一个有限状态自动机（在这种情况下，是一个Mealy机器），其中状态表示等价类，弧捕获它们之间对应的刺激-反应对。这种系统在CSP中直观地建模为一组相互递归的过程，每个过程代表一个等价类，并定义为导致代表相应等价状态的过程的刺激-响应事件对。我们首先定义CSP流程对黑盒规范建模的意义。对于一个黑盒函数BB：S→R，我们将定义一个CSP过程P，其刺激事件和响应事件分别来自S和R;因此P的字母表将是SR。对于某个跟踪tr，我们将trTS写成表示迹，其成员是也在集合S中的tr的那些成员。例如，对于某个迹线trJ和响应r，迹线tr=trJ-r表示具有响应r的刺激序列trJTS。定义3.1CSP过程P被称为对黑盒函数BB进行建模：S→R，恰好满足以下条件(i) P不得引入新行为（不在BB中）：r ∈ R·tr = tr J-r ∈R·tr BB（tr TS）= r.(ii) P必须对BB的整个域进行建模，并相应地映射每个域z∈S+;r∈R·BB（z）=r trT S = z）. 其中S+=S−{}。z=0的情况由空轨迹根据迹模型的定义，它是迹（P）的一个成员。(iii) 反映刺激-反应配对模式。由于迹（P）是prefix-封闭的，我们将其指定为：字符串：traces（P）· #（trTR） ≤ #（trTS） ≤ #（trT R）+1。P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127133其中#（trTX）返回X中的事件在跟踪tr中发生的次数。(iv) P是一个确定性过程，反映了BB是一个函数的事实。条件3是CSP模型必须遵守的黑盒规范的特征。根据相应的有限状态自动机，从任何给定的状态，只能执行刺激形式的动作，在我们的定义中没有这个性质，我们可以构造一个CSP过程P，使得εs， r， rε ∈traces（P）。假设BB（s）=r，这个迹将满足上面的前两个条件然而，这并不能准确地模拟系统黑盒规范所做的配对假设。在单个刺激确实引起一系列连续反应的情况下，人们仍然会将其捕获为单个抽象反应，以模拟它们被原子地处理并且是单个刺激输入的结果的事实。定义3.2满足定义3.1的CSP过程和基于序列的规范在编码相同的黑盒函数时被称为完全一致为了清楚起见，我们将某个规范序列ci的枚举表捕获为集合CtBB（ci），该集合CtBB（c i）包括表的每行一个元素并且采用（s， r， cj）的形式，其中s，r和cj分别表示刺激，响应和等价列。为了CSP模型的目的，我们忽略了第四列捕获非正式需求的可追溯性，因为它与系统的CSP分析无关。算法1对于给定的编码黑盒函数BB的基于序列的规范：S→R，对应的CSP过程PBB定义如下：(i) 对于枚举中的每个规范序列ci，CSP过程Pci定义如下：P CI = Q{Q（s，r，c，j）|（s，r，c j）∈<$BB（c i）}哪里Q（s， r， cj）=s→r→Pcj这产生了一个相互递归的CSP进程P c0，. ，PCn，对于枚举中的每个标准序列ci，一个过程Pci。(ii) CSP过程PBB被定义为PBB= Pc0，其中c0表示最短的标准序列，即最短标准序列。134P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127由于空间限制，我们使用下面一个非常简单的例子来说明这个算法。然而，我们将在第7节讨论我们的行业经验。例3.3考虑一台高度简化的自动售货机，它有以下几组刺激和反应：S={coin，tea，coexecute，cancel，accept}R={返回硬币，分发茶，分发咖啡，菜单，支付硬币，确认，空}假设有四个规范序列，枚举如下：c0：100c2：硬币，茶叶c1：比特币刺激响应当量硬币退币C1茶确认C2咖啡确认C3取消退币了c0接受nullC1c3：加密货币，coinee刺激响应当量硬币退币C2茶nullC2咖啡nullC2取消菜单C1接受配茶了c0刺激响应当量硬币退币C3茶nullC3咖啡nullC3取消菜单C1接受分发咖啡了c0这个枚举编码了一个完整的黑盒规范：对于任何序列z∈S，可以直接从表中导出相应的响应。空响应用于表示系统没有响应使用算法1，生成的CSP过程为P=Pc0，其中：Pc0=硬币→菜单→P c1Q 茶→支付硬币→ Pc0Q币→支付币→Pc0Q取消→空→Pc0Q接受→空→Pc0过程Pc1、Pc2和Pc3相应地从表中定义。 我们可以逐步通过P的轨迹，看看每个轨迹如何直接对应于枚举中的刺激序列-反应映射。命题3.4对于给定的编码黑盒函数BB的基于序列的规范，如果CSP过程P根据算法1构造，则P根据定义3.1对黑盒函数BB建模，因此它们是全等的。刺激响应当量硬币菜单C1茶支付硬币了c0咖啡支付硬币了c0取消null了c0接受null了c0P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127135证明简单明了，由于缺乏空间而省略。由此产生的CSP过程是确定性的，反映了黑盒规范确实是一个函数的事实。为了指定组件的设计，这种确定性模型是可行的，因为人们不会选择实现非确定性软件。这些正式设计规范的目的是确保它们在传递给实现时是完整和明确的。然而，抽象设计细节的能力在实践中是一个重要的要求。例如，在指定组件的接口并验证其交互时，必须能够隐藏内部操作。这自然导致了非决定论。CSP框架非常有效地捕获了非确定性，基于序列的指定方法为这些目的的组件提供了一种实用的方法，而不会影响其方法的功能基础。在第6节中，我们讨论了如何将我们的方法扩展到处理非决定主义。4CSP中的状态盒建模实现的下一步是从黑盒中导出一个行为上状态盒定义了一个全函数SB：（Q×S）→（Q×R），其中Q是状态集，S是刺激集，R是反应集每个状态q∈Q表示一个特征谓词∗S上由ρMe定义的等价类的χqS中的序列集合，其中χq为真。;我们写[q] ρMe 来表示在本节中，我们将说明如何在CSP中对状态盒进行建模，并提出一个构造它们的通用算法。我们首先定义状态盒函数的CSP模型要满足的迹属性定义4.1CSP过程P被称为建模状态盒函数SB：（Q×S）→（Q×R），精确地当满足以下条件(i) P不能引入新的行为（不是在SB中）：tr，trJ∈迹（P）;s∈S;r∈R·tr=trJ-s，r<$s<$q， qJ∈Q·SB（q， s）=（qJ，r）<$trJTS∈[q](ii) SB中的每个映射都由P建模：ρMe n∈[qJ]ρ我。<$q， qJ∈Q;s∈S;r∈R·SB（q， s）=（qJ，r）<$（<$tr∈traces（P）·trTS∈[q]ρMe<$tr-εs， rε ∈迹（P）<$（trTS）-ε s<$∈[qJ] ρMe）。136P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127SBJ通过归纳，这意味着SB中的所有映射都由P（因为根据迹模型的定义，迹（P）总是非空的(iii) P满足刺激-反应配对模式：字符串：traces（P）· #（trTR） ≤ #（trTS） ≤ #（trTR）+1。(iv) P是一个确定性过程，反映了SB是一个函数的事实。CSP过程的轨迹由刺激和反应组成，S和R分别，显然没有参考状态数据。这允许在对黑盒和状态盒建模的过程的迹线之间进行直接比较从基于序列的枚举的黑盒的状态盒在系统的行为方面的设计决策定义4.2一个满足定义4.1的CSP过程和一个状态盒，当它们对同一个状态盒函数建模时，被称为完全一致我们在下面提出了一个通用算法，用于将状态盒规范转换为等效的CSP模型。我们捕获在刺激s∈S的状态盒中呈现的信息，作为包含一个元素的集合并且采用（q， r， qJ）的形式，其中q是当前状态，r是状态q中s调用的响应，并且qJ是更新的状态。算法2给定一个状态盒指定函数SB：（Q×S）→（Q×R），相应的CSP过程PSB定义如下：(i) 设x1，. ，x，k表示由 状 态 盒 定 义 的状态变量。(ii) 过程PSB定义如下：P= PJ（init，.，init）SBSB1k其中init 1，. ，init k是状态变量X1，. ，x k，如状态框中所定义的。(iii) 过程PJ定义如下：SB（x1，. ，x，k）= Q{Q（s）| s∈S}对于刺激s，每个状态框有一个Q（s）。(iv) 对于每个刺激s∈S，Q（s）定义如下：Q（s）=Q{Q J（q，s，r，q J）|（q，r，q J）∈ <$SB（s）}哪里J J J JQ（q，s，r，q）=qs→r→PSB（q）对于激励s，在其状态盒中的每一行都有一个过程QJ（q，s，r，qJ）。q的值表示s调用的前提条件PP.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127137响应r和状态更新qJ，并且在CSP中被建模为布尔保护。例4.3回想一下例3.3中的简单自动售货机。考虑从该基于序列的规范导出的以下状态盒规范，其中每个等价类的特征谓词（每个由规范序列表示）由两个状态变量Coin和Drink定义如下：等价类特征谓词[]ρMeCoin=false[比特币]ρMe硬币=真饮料=无[币，茶]ρ我硬币=真硬币饮料=茶[cocoin， cocoin]我Coin=true饮料=coin其中，硬币和饮料是用值的范围{true， false}定义的，{无，茶，咖啡}分别。状态盒表（每个刺激对应一个）来自例3.3中的枚举表和上面定义的特征谓词。例如，（忽略第4列Trace规则）刺激tea和cancel的状态框定义为：刺激：茶当前状态响应新状态Coin=false支付硬币没有更新硬币=真饮料=无确认饮料=茶硬币=真硬币/=无null没有更新刺激：取消当前状态响应新状态Coin=falsenull没有更新硬币=真饮料=无退币Coin = false硬币=真硬币/=无菜单饮料=无假设Coin和Drink的初始值分别为false和none，CSP过程定义为PSB=P（false， none），其中：P（c，d）=<$c&硬币→菜单 →P（真，d）Q c&硬币→返回硬币→P（c，d）Q？c&？x：{tea，co_coin} →pay coin→P（c，d）Qcd =无？x：{tea，co_（？）} →confirm→P（c，x）Q cd/=无？x：{tea，co_xee} →null→P（c，d）Q <$c&cancel→null→P（c，d）Qcd=nonecancel→return coin→P（false，d）138P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127Q c无&取消→菜单→P（c，无）Q <$cd=无接受→空→P（c，d）Q cd/=无&接受→分配。d→P（false，none）每个受保护的选择都直接从状态盒表中导出。例如，选项3、4和5分别来自茶和咖啡的表格命题4.4对于一个给定的状态盒，它编码一个完整的、一致的状态盒函数SB，如果一个CSP过程P是根据算法2构造的，那么P根据定义4.1对SB建模，因此它们是全等的。证明简单明了，由于缺乏空间而省略。5使用FDR进行在本节中，我们简要总结了我们在FDR中使用该框架在行业中进行的分析。在设计的盒结构开发的每个阶段，一旦在CSP中对规范进行建模，则可以使用FDR来制定和验证系统需求中指定的完整性、确定性和控制律等属性在状态框中需要验证的另一个要求是，定义为状态数据的特征谓词是不重叠和完整的。在实践中，这一阶段的错误经常被引入。这两个属性在FDR中都很容易检查：第一个是通过检查非确定性来捕获的;如果有重叠的谓词，那么对于给定的刺激s，将有一个状态，其中至少有两个警卫评估为真，导致关于执行其中哪一个的不确定性选择。如果我们想区分两种情况下的结果响应和状态相同的情况，那么可以自动向模型添加额外的事件，以确保该错误仍然被捕获为不确定性行为。第二个属性可以用公式表示为活性条件，也可以使用FDR进行验证。行为等效性盒子结构定义中的每一步都必须经过验证。关于黑盒和状态盒，必须验证它们在行为上是等价的（如2.1节所定义）。通常，通过从状态盒中导出黑盒行为并检查其是否等同于原始黑盒规范来完成此验证。这在实践中是耗时且不可行的。这里提出的算法允许将这两种规格转换为相应的P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127139CSP模型，并在FDR中自动完成必要的验证检查。使用定义3.1和4.1，如上所定义的基于序列的规范和状态盒规范之间的行为等价性可以根据相应CSP过程的迹来公式化：当它们各自的CSP模型PBB和PSB是迹等价的时，基于确定性序列的规范SpecBB和确定性状态盒规范SpecSB这是使用FDR自动检查的。如果检查失败，则FDR生成反例;由于CSP跟踪与BSDM中的表格表示之间的密切相关性，反例在任一框架中都易于理解。盒子结构方法在设计开发中是以组件为中心的我们通常使用它来开发组件的设计和接口规范，一旦软件架构师完成了整体结构并将其分解为单个组件。通过将它们转换为CSP，我们能够根据所提出的体系结构将它们并行放置，并正式验证整个系统。诸如死锁、组件是否相互调用非法行为以及控制律等属性在CSP中制定，并在FDR中自动验证。CSP的组合特性为这种开发提供了可扩展性。6处理抽象在[7]中，提出了许多有效的抽象技术，以避免基于序列的指定方法（用于构造黑盒）中的过度指定。我们简要总结了我们的方法如何扩展到处理我们在工业中使用的两个为了避免序列枚举中的过度指定，可以通过多种方式抽象细节，例如，通过引入抽象刺激（而不是用系统的实际具体刺激指定完整的枚举）。然后，必须证明这两种表示在行为上是等价的。这种抽象通常涉及将序列从不同的等价类映射到单个序列，并在其上定义谓词以捕获其独特的特征。然后，当需要这种详细程度时，可以定义这些谓词。例如，考虑自动售货机，其中分配饮料涉及检查多个资源的可用性。列举这一点并为每个组合确定不同的等价类是不必要的。140P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127另一种方法是抽象出这种细节水平，并引入谓词p，该谓词p确定是否有足够的资源来分配给定的饮料d这种谓词通常是根据刺激序列上的前缀递归函数来定义的。在这种情况下，p可以被定义为Resource（h）/=p，其中Resource（h）在刺激序列h上被定义并且返回可用资源的集合。一个刺激s，其反应依赖于这个谓词（例如，tea），然后由特殊的抽象刺激s：p和s：<$p来建模。例如，给定规范序列c的枚举表可以使用这些抽象刺激定义如下：刺激响应当量迹规则s：Resource（h）=/∅分发Ci...s：资源（h）=1000不可用CJ...其中，必须为等价类中的所有刺激序列定义资源，该等价类的特征为规范序列c，h表示枚举表中列出的所有刺激之前的刺激序列历史完整性和一致性是通过确保谓词及其否定在同一序列上定义来实现的详情见[7]算法1可以扩展到处理在刺激历史上定义的谓词，通过引入状态变量来捕获基本信息（与状态框指定的方式相同）。不是参考序列历史，而是根据CSP模型中相应的状态数据计算谓词。形式为s：p的枚举表中的每个刺激s都被建模为具有布尔嘉德山口 例如，对于上表，我们将有：P（res）=resQ&注射→分配。s→Pci（f（res））res= 0 &s →不可用。s → P cj（g（res））其中res是状态变量，函数f和g表示由Resource定义的状态更新。欠规范化基于序列的规范化方法使用预测来实现欠规范化的黑盒规范化[7]（而不破坏该方法所基于的函数理论）。在实践中，这是抽象的一种基本形式，既用于指定组件接口，其中内部操作对其环境隐藏，也用于指定设计将被验证的需求。在黑盒抽象层次上的具体化是通过引入P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127141未定义的谓词来捕捉这样一个事实，即对于给定的刺激s，存在许多可能的反应和随后的行为，其决定尚未定义。在正在进行的研究中，我们正在考虑削弱定义3.1并扩展算法1，以构建相应的CSP模型并捕获潜在的不确定性。例如，对于以下形式的抽象刺激：刺激响应当量迹规则S：pR1Ci...s：<$pR2CJ...其中p是未定义谓词，CSP过程定义如下：P=（s→r1→Pci）Q（s→r2→Pcj）从而潜在地导致在执行S之后的非确定性（取决于后续响应和行为是否不同）。在实践中，我们可以使用这种方法指定系统的组件接口，并通过使用CSP细化来验证所提出的设计（从BSDM转换为CSP）是否满足FDR的预期接口。由于细化的传递性和CSP运算符相对于细化的单调性，CSP支持组合开发，使这种方法能够在实践中扩展。当在CSP模型中对不确定性进行建模时，故障模型用于所有细化。7结论在本文中，我们概述了如何将BSDM和CSP结合起来，以在实践中获得两者的好处。 我们提出了将黑盒和状态盒规范转换为CSP的通用算法，并简要讨论了如何将这项工作扩展到处理抽象技术，如欠规范。我们使用这种方法来增强软件系统的设计，并在实施阶段开始之前对其进行验证;在实践中，设计错误往往是最昂贵的解决（在资源和时间方面），只有在测试阶段才能发现有一些优势，我们提出的组合方法比一些传统的形式化方法，包括CSP使用自己的。第一个是它整合到一个有组织的工业环境中的范围，这是通过BSDM和基于序列的规范方法实现的。它是实用的，因为它提供了正式规范和非正式需求之间的可追溯性，软件工程师和领域142P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127我们认为，这种方法不需要大量的培训，而且根据我们过去两年在行业中使用这种方法的经验，它已被证明具有良好的扩展性（其他人的经验参考可在[8]中找到）。其次，使用BSDM开发的规范可以翻译成其他形式语言，在我们的例子中是CSP，因此它可以作为引入形式验证方法的有效桥梁。最后，模型检查器FDR提供了实践中所需的必要的自动化工具支持。 这还包括在分析过程中发现的设计错误的有效和有意义的反馈由于BSDM中的表格表示与CSP中对应的迹线描述之间的相似性，只要为系统中每个组件的刺激和响应选择合理的命名约定，就工业经验我们已经使用这种组合方法来开发复杂的、事件驱动的嵌入式控制软件，以控制复杂的制造机器。它已被证明是成功的和可扩展的新组件的开发和现有软件组件的重新设计。例如，我们的一个应用程序涉及到设计和实现一个基于22个无头PC平台的机器的过程控制内核，该平台并行运行，并通过内部以太网相互通信。内核被设计为两个并发进程，即机器控制器和状态控制器进程，通过队列进行通信。机器控制器实现机器的基本操作行为并控制其他主要子系统。它负责机器的一致性和执行管理安全操作的控制规则它使用由它控制的子系统提供的接口，并实现了一个仅由状态控制器使用的接口。状态控制器实现了GUI组件以及机器操作员所看到的整体机器行为。机器控制器设计的黑盒功能在47个等价类中有2，835个映射。最长典型序列的长度为11个刺激。状态控制器设计的黑盒函数有837个映射，最长规范序列的长度为6个刺激。除了将内核组件的设计定义为黑盒之外，它们实现的接口和它们使用的接口也被定义为未指定的黑盒。使用本文提出的算法将这些规范转换为CSP，使得FDR能够自动执行以下验证：（i）两个内核进程的设计是确定的，并正确实现了各自的接口;（ii）状态控制器和代表接口的进程的P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127143的机器控制器是死锁自由和正确的行为根据机器控制器完成的内核大约有20，000行C++可执行代码。规格、设计及实施工作约为16个人工周。最终代码在一天内集成到目标机器上。 在密集使用的前4周，发现了8个轻微的编码错误，其中没有一个是规范或设计错误;在此后的12个多月里，没有发现其他错误。到目前为止，返工率低于1%。未来的工作我们目前正在正式的工作总结在第6节和扩展我们的方法与其他实际的抽象技术。目前还在进行关于队列等结构的有效建模的研究;我们正在寻求根据适合于每种模式的建模技术对常见的设计模式和过程关系进行分类。其他感兴趣的途径是：使用FDR实现枚举规范中不同抽象级别的自动验证（例如，抽象与具体刺激）;将我们的方法从状态框扩展到BSDM中的清除框;并在此框架中对实时系统进行建模。确认我们感谢Bill Roscoe和Michael Goldsmith对这项工作进行了有益的讨论和评论这项研究由荷兰Verum Consultants资助。引用[1]J. R.阿布里尔B书：将程序转化为意义。 剑桥大学出版社，1996年。[2]Formal Systems（Europe）Ltd.Failures-Divergence Refinement：FDR2 User Manual，2003. [3] C. A. R.霍尔通信顺序进程。普伦蒂斯·霍尔1985年[4] G. J. Holzmann。模型检查器旋转。IEEE软件工程学报，23（5）：279[5] H. D.米尔斯在箱式结构系统中逐步完善和验证。Computer，21（6）：23[6] H. D.米尔斯河C. Linger和A. R.海夫纳信息系统分析与设计原理。中国科学院出版社，1986年.144P.J. Hopcroft，G.H.Broadfoot/Electron.注意Theor。Comput. Sci. 128（2005）127[7] S. Prowell和J.H.可怜。基于序列的软件规范的基础。IEEE Trans. of Soft. Eng. ，29（5）：417[8] S. J. 普罗韦尔角J. 特拉梅尔河C. Linger和J.H. 可怜。净室软件工程- 技术和过程。 Addison-Wesley，1998年。[9] A. W.罗斯科模型检查CSP。在一个经典的头脑：散文在荣誉C.A.R.霍尔，第353-378页。Prentice-Hall，1994年。[10] A. W.罗斯科 并发的理论与实践。 Prentice Hall，1998年。
我的内容管理
展开
