飞行制导系统模型检测：SPIN v.s. NuSMV 的优劣和优化方法

理论计算机科学电子笔记133（2005）61-79www.elsevier.com/locate/entcs模型检测飞行制导系统：从同步到异步崔妍子弗劳恩霍夫实验软件工程研究所，德国摘要模型检测已经成为一种很有前途的自动验证技术。尽管如此，大多数现有的模型检查器都是专门针对系统的有限方面的，其中每个模型检查器都需要一定的专业知识水平才能以正确的方式在正确的领域中使用工具。几乎没有任何指导方针可用于为特定问题域选择正确的模型检查器，这使得在实践中采用该技术更加困难。基于作者在Rockwell-Collins的商用飞行制导系统（FGS）上使用符号模型检查器NuSMV的经验，研究了在同一问题上使用显式模型检查器SPIN的相对优点和缺陷。这是罗克韦尔-柯林斯项目一开始就提出的一个问题。挑战包括有效地使用SPIN的复杂的同步模式逻辑与大量的状态变量，其中SPIN是已知的是不是特别有效。最后给出了SPIN模型的优化方法，避免了状态空间爆炸的问题，使SPIN模型的扩展性能优于NuSMV模型，并讨论了结果的意义。 我们希望我们的经验可以为将来在类似领域中使用模型检测关键词：模型检验，飞行制导系统，SPIN v.s. NuSMV1介绍模型检查[4，15]已成为软件和硬件系统自动验证的一种有前途的在实践中应用该技术的一些成功案例[2，9，10，12，14，21]的激励下，明尼苏达大学的关键系统研究小组将符号模型检查器NuSMV [22]集成到以规范为中心的系统开发中。1电子邮件：choi@iese.fraunhofer.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.05862Y. 崔/理论计算机科学电子笔记133（2005）61环境Nimbus [13]。集成模型检查器已成功地完全用于检查数百个商用飞行制导系统（FGS）规范的要求属性，飞行控制系统的一个组成部分，在罗克韦尔柯林斯[3，21]。该项目的成功对于形式化方法的实践具有特别的意义，因为FGS的所有需求工程活动，从编写规范到进行形式化验证，都是由Rockwell-Collins的从业人员执行的。然而，从项目开始以来，正确的模型检查器的选择一直是一个问题;在应用领域中对各种模型检查器的比较研究尽管该项目取得了成功，但我们一直在想，其他选择是否会更好。特别是，符号和显式模型检查之间的选择是相当不清楚的，只有有限的比较参数;其中，有人认为，符号模型检查执行更好的同步系统与硬件一样的特点和显式模型检查是更好的异步系统与一些通信进程。然而，许多报告指出，直接比较这两种技术是非常困难的，如果不是不可能的[1，7，16]。一些实验报告说，符号模型检查器甚至在异步系统中也表现得更好[7]，这与一些论点相矛盾。此外，一个系统可以同时具有同步和异步两个方面，这取决于我们感兴趣的部分以及我们如何解释系统行为。例如，FGS系统由并行运行的两个FGS组成，一个主动FGS和一个用于备份的被动FGS。当我们考虑它的两个通信进程并行运行时，该系统是一个异步系统;当我们只关注单侧FGS的模式逻辑时，它可以被解释为一个同步系统，其复杂的模式逻辑复杂到足以挑战模型检测技术我们已经研究了在FGS上使用SPIN [17]我们介绍了SPIN模型检查器在FGS规范上的应用，并将结果与我们之前报道的NuSMV进行了比较[3，21]。这项工作涉及到将同步规范转换为用于指定通信过程的建模语言的挑战我们的直接翻译显示了SPIN的灾难性性能，即使在小尺寸的FGS上也会迅速爆炸。这个问题主要是由于大量的全局和局部变量，包括历史值，访问系统模型和其环境模型。在仔细检查之后，我们封装了尽可能多的变量，Y. 崔/理论计算机科学电子笔记133（2005）6163在每个进程中尽可能多地使用共享变量，并使用消息传递机制来允许其他进程访问共享变量的值结果非常令人鼓舞; SPIN能够在合理的时间内检查FGS模型上的属性此外，相同的方法使得可以验证关于两个通信FGS的重要属性-相同的属性NuSMV无法按比例放大以检查。我们的优化是系统性的，并执行最小的更改，以支持验证过程的自动化。考虑到这种最小优化带来的性能增益，我们相信还有更多的空间来进一步提高性能。换句话说，在处理大规模系统时，SPIN可能比NuSMV更灵活，但也可能更难由非专家使用，因为优化可能在可用性方面提出几个问题：（1）基于属性的优化需要不同属性的不同模型，这在检查数百个需求属性时可能是一个问题，以及（2）更积极的优化可能会提高性能，但可能导致原始模型的急剧变化。这使得建模者难以理解。我们相信，任何优化方法都必须是系统化的，以便可以自动化，在原始模型和优化模型之间提供可跟踪性。这是我们今后调查的重点。本文的其余部分组织如下：第2节讨论了现有的相关工作，重点是比较符号和显式模型检查技术。第三节介绍了我们的动机，简要描述了现有的工作有关的模型检查飞行制导系统。第4节描述了我们对SPIN模型的直接和模块化转换及其性能数据。最后，我们讨论第5节中结果的含义。2相关工作符号模型检查与显式模型检查的利弊一直是争论的主题，但没有得出结论性的结果。困难是由于给定问题的理论性能分析是不可能的;符号模型检查的最佳变量排序是NP完全问题，因此在显式模型检查的偏序约简应用中计算最佳约简[17]。这两种技术都使用了启发式，让我们别无选择，只能“试试看”。在文献[1]中，对绩效比较的困难和实证研究的重要性进行了充分的论述。关于这一问题，在不同领域有一些比较报告64Y. 崔/理论计算机科学电子笔记133（2005）61在[6]中，在GNU uucp 1.04版的i协议模型上比较了SPIN、SMV和XMC，结果表明XMC优于其他两个模型检查器。 结果证实了一个众所周知的论点，在异步协议验证方面，显式模型检查器的性能优于符号模型检查器。有趣的是，SPIN的发明者Gerard Holzmann已经改变了这一结果，并通过对SPIN模型的仔细优化进行了逆转[16]。这种情况清楚地表明了在不同的模型检查器之间进行公平比较的困难以及优化的重要性，这需要高水平的专业知识。他们最近的出版物[5]在同一问题域中对各种显式模型检查器进行了更全面的比较。在使用符号模型检查器RULEBASE和显式模型检查器SPIN验证磁盘控制器的软件时，Reynner和Peled研究了另一个众所周知的论点，即符号模型检查更适合硬件系统，显式模型检查更适合软件系统[7]。他们的结果表明，RULEBASE能够对具有10150个状态的2进程系统进行模型检查，而SPIN在使用2G内存检查108个这一结果不利于明确的模型检查执行更好的软件验证，特别是通信过程的论点。此外，还对Murφ、SMV和SPIN在分析飞行制导系统模态混淆方面的性能进行了比较[19]。每个模型检查器的翻译描述使用一个例子，每个工具的优点和缺点进行了讨论，就其可用性。还指出了SPIN中状态空间爆炸的可能性，特别是因为内联用于其翻译中的所有过程。据我们所知，这是我们感兴趣的领域，即飞机控制系统中唯一的比较研究。然而，案例研究中使用的模型由于我们没有可扩展性的分析数据，我们无法从这个小案例研究中得出结论。3背景罗克韦尔-柯林斯公司与明尼苏达大学合作进行了一项案例研究，以确定是否可以使用形式化方法以合理的成本对系统要求进行验证。一系列的飞行制导系统已被指定使用正式的规格化语言RSML-e（无事件的需求状态机语言）[25]，使用RSML-e执行提供的可视化和仿真工具进行Y. 崔/理论计算机科学电子笔记133（2005）6165乘务员接口飞行管理系统传感器数据管制法律自动驾驶致动器数据模式逻辑飞行制导系统Fig. 1. 飞行控制系统环境NIMBUS [13]，并通过全自动翻译使用NuSMV模型检查器和orem证明器PVS [23]验证数百个功能和安全要求，发现模型中的许多错误[21]。该项目非常成功;正式方法的使用，包括编写正式规范和使用NuSMV进行验证，是由罗克韦尔-柯林斯公司的人员进行的，明尼苏达大学的研究人员几乎没有帮助。 该项目的第一阶段得出的结论是，3.1飞行制导系统飞行制导系统（FGS）是飞行控制系统的一个组成部分（图1，借用自[19]）。它将飞机的测量状态与期望状态进行比较，并生成俯仰和滚转制导命令，以最小化测量状态与期望状态之间的差异。期望状态由机组接口和/或光管理系统与系统的当前状态一起确定。制导指令由模态逻辑选择的控制律算法计算。模式逻辑确定在任何给定时间哪些横向和垂直模式处于待命状态和激活状态[20]。FGS包括相同的左侧和右侧，其中只有一侧是活动的，负责输入和产生输出。非活动端只是从活动端复制其内部状态，作为热备份（图2）。FGS的复杂模式逻辑是嵌入式控制系统设计中经常遇到的一类问题的代表有关FGS模式逻辑的更详细描述，请参见[20]。罗克韦尔的人用RSML-eCollins在项目的最后阶段为单侧FGS提供了大约3，500行（带注释）。它包括13个通过机组接口的输入开关，82个代表系统内部状态的枚举变量，以及123个66Y. 崔/理论计算机科学电子笔记133（2005）61输入接口输入开关输入开关图二. 双面飞行导引系统宏。请注意，RSML-e提供了宏和函数构造来提高规范的可读性。在FGS规范中，宏被广泛地用作同步事件的替代表示，最终，它提供了一种简洁的方式来指定时态逻辑2中的系统属性。由于宏封装了复杂的模式逻辑，在时序逻辑规范中使用宏极大地简化了逻辑表达，这对增强模型检测的可用性起着至关重要的作用。在RSML-e规范自动翻译成NuSMV输入语言后，使用模型检查器NuSMV（版本2.1）以批处理模式验证了总共298个属性每个属性取决于性质和是否产生反例，从几分钟到两小时不等。在最后阶段，当模型中的所有错误都被纠正后，NuSMV在大约1.5小时内在800 MHzLinux机器上用512 M内存验证了所有298转换和模型检查过程是完全自动化的，除了需求属性被手动转换为时态逻辑并附加到生成的NuSMV文件。3.2这项工作成功使用全自动核查器核查数百个物业，令人鼓舞。然而，FGS的大小几乎达到了NuSMV的极限;它需要积极的抽象来扩展到更大的系统。 事实上，验证一直集中在FGS的一边，使用关于另一边的假设作为不变量。这些不变量由工程师手动识别，并施加在NuSMV上2系统属性需要在时序逻辑中指定[24]以便进行模型检查。FGS左侧电流模式转移FGS右侧FGS左侧电流模式FGS右侧输出接口Y. 崔/理论计算机科学电子笔记133（2005）6167模型直接如图3所示，FGS模型仅包含一个初始激活的侧，并且每当按下转换开关时激活/停用。激活时，它根据当前模式和输入值计算FGS的模式。当处于非活动状态时，它会复制另一端的模式，作为具有一些不变量的随机输入之所以采用这种方法，是因为所识别的需求主要涉及FGS功能中的模式逻辑，可以在同步假设3下使用单侧FGS通过假设保证推理进行检查确认和验证活动是增量的，从非常抽象的FGS到细化的全尺寸FGS，主要是由于缺乏关于模型检查可扩展性的信息。NuSMV成功扩展到全尺寸单侧FGS，但尚未成功扩展到双侧通信FGS。从经验来看，很明显，符号模型检查可以非常强大，也可以使用，但只能达到一定的程度。该技术是基于穷举状态空间搜索，并不提供替代方案时，它达到其限制。另一方面，显式模型检测通常提供更多的灵活性，在处理一个大的状态空间，有时交易的效率穷举。我们希望显式模型检查的扩展能够为我们提供一定程度的验证能力，即使是对于符号模型检查无法处理的较大系统。为了实现我们的希望，我们设定了两个调查目标;第一个是检查使用显式模型检查器SPIN来验证FGS的可能性，第二个是提出一个本文介绍了一种将RSML-e翻译成SPIN输入语言的系统方法，支持完全自动化和更好的可用性，如果第一个目标是可以实现的。4基于SPIN的我们开始从翻译的RSML-e模型的单侧FGS 与不变量的输入语言的SPIN，Promela。 我们的直觉假设-SIS是SPIN必须能够处理同步单侧FGS，以便缩放到双侧异步FGS。 我们的第一次直接翻译的尝试对于模型检查来说太低效了。为了达到更好的性能，我们采用模块化和封装，利用SPIN消息传递机制和修改宏来应对结构的变化。变化的结果是相当有希望的;它[3]同步假说认为，底层机器是无限快的，因此，系统对输入事件的反应是瞬时的[8]。68Y. 崔/理论计算机科学电子笔记133（2005）61输入开关FGS如果活动基于输入开关的计算模式其他复制其他FGS对其他FGS的其他FGS输出接口输入接口图三. 单侧飞行制导系统与NuSMV相比，SPIN能够以可容忍的时间和内存成本对单侧同步FGS进行模型检查相同的结构化和模块化方法使SPIN能够扩展到双侧异步FGS，这对于NuSMV是不可行的。4.1基于SPINRSML-e [25]是一种同步状态机语言，在语义上类似于Lustre [11]，SpecTRM-RL [18]和SCR [14];状态变量表示系统在给定时间的当前状态，其中状态变量的值基于通过输入接口接收的输入变量值和状态变量的先前值（系统配置）计算新计算的状态变量值可以通过输出接口发送出去通过输出消息。在RSML-e中，所有变量都有一个全局作用域，RSML-e模型被认为是开放的，这意味着系统正在与其开放的环境进行交互。我们的第一个挑战是在SPIN的建模语言Promela中对具有大量变量和复杂模式逻辑的同步系统进行建模。如前所述，FGS规范包括13个输入变量、82个状态变量和123个宏。此外，大多数宏引用状态变量的历史值，因此，模型需要记住变量history的值。虽然历史的深度被限制为1（到前一个值），但它使跟踪系统状态所需的变量数量增加了在普罗梅拉，它是-需要至少2×（13 + 82）个变量来跟踪所有必要的值。对于初始方法，我们执行了RSML-ePromela旨在实现自动化翻译，就像我们为NuSMV 翻译所做的那样。RSML-e基本结构、状态变量、输入变量和宏被转换为Promela变量和C风格的宏Y. 崔/理论计算机科学电子笔记133（2005）6169输入消息输入接口输出消息输出接口输入变量自己的输入来自其他FGS的状态变量状态转换宏函数输入变量输入历史变量宏输入通道输出通道环境过程输入值的非确定性主要工艺状态变量历史变量状态转换(a) 基本RSML-e构建体（b）Promela翻译见图4。 基本RSML-e结构及其到Promela如图4所示。第二个挑战来自于这样一个事实，即SPIN需要一个封闭的系统，其中所有系统与其环境的交互都必须明确指定。如图4所示，我们通过引入另一个进程显式地对系统环境进行建模。因此，翻译后的模型有两个过程，一个是FGS本身，另一个是环境。通过在环境进程和实际FGS进程之间使用握手消息传递机制，输入变量和消息通道在Promela中被声明为全局变量，因为FGS模型和环境模型都可以访问这些变量。FGS过程将FGS状态变量及其对应的历史变量转化为局部变量，并利用Promelaif语句对它们之间的转换关系进行转换。用户定义的枚举类型被转换为Promelamtype。宏在Promela中被声明为C风格的宏;SPIN为C风格的宏执行预处理，因此不会为宏引入额外的变量虽然基本的翻译是直接的，但存在两个Promela特定的问题：首先，系统的环境必须明确指定。这意味着我们必须以非确定性的方式对所有13个输入变量的可能值进行建模，以模拟来自开放环境的随机输入。其次，为了对只有一侧的FGS进行建模，我们还必须明确地对来自具有约束的其他FGS的可能输入进行建模。幸运的是，对于布尔或枚举变量，纯非确定性输入的建模相对简单，因为Promela70Y. 崔/理论计算机科学电子笔记133（2005）61if语句支持非确定性。例如，对于航向开关HDG，非确定性输入值分配可以如下进行：如果：：1-> HDG =开;：：1 ->HDG=关闭;fi;然而，Promela不支持对模型本身施加不变量，因此，对来自另一端FGS的非确定性输入值施加约束可能非常棘手。一种方法是用约束来限制非确定性的赋值，并使用断言语句或LTL验证器来检查模型是否实际满足约束。例如，以下是在来自另一侧FGS的输入值中要满足的假设，以及在NuSMV中将其作为不变量施加的方式。- 如果另一侧FGS的模式为On，则选择ROLL或HDG或在另一侧FGS中选择NAV。- INVAR其他FGS模式=打开→其他FGS滚动=选定|其他FGS HDG =选定|其他FGS NAV =已 选择在Promela中，此不变量在环境模型中手动强制执行，以便环境不会生成不遵守约束的输入值。图5显示了FGS版本的一小部分翻译后的Promela代码;图左侧的上半部分包含宏声明、变量值的消息类型声明和输入变量声明的示例。左侧的下半部分显示了生成带有约束的随机输入值的环境进程的一部分。图右侧的上半部分显示了状态变量及其历史变量在FGS过程中的声明方式。FGS的采样模式逻辑规格见下半部分。结果性能非常差;当检查关键属性时，SPIN会迅速占用内存，P1. 当且仅当选择ROLL（翻滚）或HDG（航向）时，模式通知开启选择或选择NAV验证在800 MHz Linux机器上进行，内存为768 M我们在SPIN中将内存限制设置为600 M。使用带有压缩功能的hash-compact选项，验证过程在24分钟后终止，实际使用625 M内存。最大搜索深度设置为1，000，000，但SPIN报告搜索深度太小。其他SPIN验证选项的情况类似或更糟。结果Y. 崔/理论计算机科学电子笔记133（2005）6171// macros（总共123个宏）#define When_FD_Switch_Pressed（FD_Switch == OnPREV_STEP_FD_Switch！= 开）#定义When_Turn_FD_Off（当_FD_Switch_Pressed_Seen超速时！=1）#定义When_FD_Switch_Pressed_Seen（When_FD_Switch_PressedNo_Higher_Event_Than_FD_Switch_Pressed）：//枚举类型声明mtype = {关闭，打开，清除，选择，武装，活动，未定义，完成，左，右，脱离，锁定，捕获，跟踪};//输入变量（总共13个输入变量，// 13个输入历史变量）mtypeFD_Switch =未定义; mtypeHDG_Switch =未定义;：bool Offside_FD_On;bool Offside_Modes_On;bool Offside_Roll_Selected;：proctype env（chan input1，out）{ do：：1->//初始非确定性赋值如果：：1 -> FD_Switch = On;：：1 -> FD_Switch =Off; fi;：//在另一侧FGS上施加不变量，：：1 -> Offside_Modes_On = 0;Offside_Roll_Selected =0;Offside_Hdg_Selected=0;Offside_Nav_Active =0;：：1 -> Offside_Modes_On = 1;Offside_Roll_Selected =1;Offside_Hdg_Selected=0;Offside_Nav_Active =0;：：1 -> Offside_Modes_On = 1;Offside_Roll_Selected =0;Offside_Hdg_Selected=1;Offside_Nav_Active =0;：：1 -> Offside_Modes_On = 1;Offside_Roll_Selected =0;Offside_Hdg_Selected=0;Offside_Nav_Active =1;return 1;proctype FGS（chan input，out1）{// FGS状态变量（总共82个状态变量）mtypeOnside_FD = Off;bool Onside_FD_On = 0;mtype Modes = Off;mtype ROLL =未定义; boolFD_Cues_On = 0;：//历史变量（共82个历史变量）mtypePREV_STEP_Modes = Undefined; mtypePREV_STEP_ROLL = Undefined;：//模式逻辑：如果- -！Is_This_Side_Active->Onside_FD = Offside_FD;：：（Onside_FD == Off）When_Turn_FD_On-> Onside_FD =开;：：（Onside_FD == On）When_Turn_FD_Off->Onside_FD =关闭;：：else ->skip; fi;Onside_FD_On =（Onside_FD ==On）;如果：：Is_This_Side_Active！= 1->Modes = Offside_Modes;：：（Modes ==Off）When_Turn_Modes_On&&Is_This_Side_Active->Modes = On;：：（Modes == On）When_Turn_Modes_Off&&Is_This_Side_Active->Modes = Off;：：else -> skip;fi;：}fi;：}图五. FGS从RSML-e到Promela72Y. 崔/理论计算机科学电子笔记133（2005）61考虑到模型中变量的数量以及显式模型检查处理系统状态空间的方式，这并不令人惊讶。4.2通过模块化进行优化FGS的直接转换版本的状态空间爆炸的主要来源特别是，全局变量在SPIN验证中是昂贵的，因为SPIN需要在状态转换图中跟踪它们的所有值为了优化性能，我们研究了机械方法来最小化全局变量和局部变量的数量。请注意，我们在这项研究中的目标之一是在实践中支持可用的验证过程，因此，出于优化目的对原始模型的任何修改都需要系统化，以便可以自动化 在今后的工作中。从概念上讲，输入变量可以被认为是FGS状态机的一部分，也可以被认为是生成输入变量值的环境模型的一部分。从这个意义上说，我们应该能够在环境进程中将输入变量声明为局部变量，并将它们传递给另一个进程通过消息通道，通过模块化每个进程消除所有全局变量。不幸的是，这并不像听起来那么简单，因为输入变量及其历史值由宏引用，宏又由FGS状态转换引用;env必须能够更新输入变量，并且FGS进程必须能够通过宏访问这些变量值。例如，在FGS过程中，状态变量Onside FD的转换条件中引用When Turn FD On宏（图5）。 宏指的是宏“当FD开关按下时看到”再次引用宏“当FD开关按下时”和“没有高于FD开关按下的事件”。这些final宏引用输入变量值，如FD Switch。处理这种宏用法的一种可能方法是预处理所有宏，将规范中对宏的所有引用替换为它们的值表达式。然而，这些宏是由从业者以某种方式指定的，以匹配他们与飞行员交流时使用的语言，并且许多要验证的属性（298个中的98个）都是以宏名称的形式指定的。因此，我们不想改变他们，如果不是真的有必要4。4我们需要将宏转换为变量，就像我们在NuSMV翻译中所做的那样，以便能够检查使用宏名称指定的属性。然而，这超出了本文件的范围，我们将其留给今后的工作。Y. 崔/理论计算机科学电子笔记133（2005）6173(a) 使用原始宏的模块化方法（b）使用修改后的宏的模块化方法见图6。 模块化翻译方法我们可以使用Promela消息传递机制，以便通过使用宏实现模块化;所有输入变量都可以在env进程中声明为局部变量，并且所有值都可以通过消息通道传递给FGS进程。我们在FGS过程中单独声明输入历史变量作为局部变量，以减少通过消息通道传递的消息数量。然而，为了使用宏，我们需要保留传递的消息值的名称，这在Promela中可以通过在FGS进程中创建消息的本地副本或为每个变量创建一个消息通道来实现（图6）。这两种情况都是昂贵的，因为创建消息的本地副本会增加变量的数量，并且消息通道在Promela中总是被视为全局变量。为了实现更好的优化，我们根据以下四个类别对宏进行分类：（1）其值仅由参考树深度为1的输入变量值确定的宏，（2）其值仅由参考树深度大于1的输入变量值确定的宏，（3）其值由FGS过程中本地声明的状态变量确定的宏，以及（4）其值由输入变量和状态变量值确定的宏。基于这种分类，我们执行以下三种类型的优化。类别1：我们将宏中引用的输入变量名更改为从env进程传递到FGS进程的相应消息字段名类别2：我们在env进程中为每个宏宏环境过程输入变量自己的输入其他FGSFGS工艺状态变量历史变量状态转换输入变量的副本输入历史变量宏组1宏组2宏组3宏组4环境进程消息自输入消息其他FGS的输入消息FGS工艺状态变量历史变量状态转换输入历史变量消息通过消息通过74Y. 崔/理论计算机科学电子笔记133（2005）61因此，可以在同一过程中对其进行评估，并通过消息通道将其传递给FGS第3类：无变动。第4类：我们修改在这个类别中的宏中引用的名称，以反映通过消息通道和第2类中宏的转换来改变输入变量的名称。通过第1类中宏的方法，我们不需要为输入变量值保留本地副本，减少了本地副本的数量。cal变量 例如，当FD开关按下时的宏定义从（FD开关==打开）&&PREV STEP FD开关！=打开）至（值.msg[0]==打开&&PREVSTEP FD开关！= 因为FD Switch是env进程中声明的一个输入变量，其值通过消息通道传递给FGS进程（图7）。values是传递用户定义的消息类型msg的消息通道的名称，msg是一个mtype数组。第二种方法是将不能用简单方法处理的复杂宏处理为第1类。 例如，上一页中描述的When Turn FD On宏有一个引用树深度3我们可以遍历引用树中引用的名称，并更改它们以反映第一种方法中的更改。相反，为了简单起见，我们在env通过这种方式，所有引用都在env模块中解析，只有结果值将传递给FGS进程（参见图7中的proctype env内部）。类别3中的宏不需要更改，因为所有宏都在FGS进程中引用，其中所有状态变量都声明为局部变量。 用于类别4中的宏的方法组合了用于类别1和类别2中的宏的方法。图7是基于该方法的FGS的模块化翻译的一部分，其示出了图5中所示的模型的相同部分，用更大的字体突出显示了改变的部分。这些优化方法使SPIN能够在20分钟内使用位状态散列选项验证属性P1;它探索的搜索深度为8，133，它探索的状态和转换总数为2。1 × 10 7和2。9×107。总共消耗了9.938 M内存我们所有的实验都默认使用偏序约简相比较而言，使用NuSMV在10秒内以24 M的内存消耗验证相同的属性。然而，使用穷举搜索算法对于该模型仍然是不可行由于位状态散列算法执行状态空间的部分搜索，结果可能是不可靠的。Y. 崔/理论计算机科学电子笔记133（2005）6175// macros（total 123 macros）#define When_FD_Switch_Pressed（values.msg[0]==打开&&PREV_STEP_FD_Switch！= 开）#define When_Turn_FD_Off(When_FD_开关_按下_可见&&values.msg[10]！=第一章#define When_FD_Switch_Pressed_Seen(When_FD_Switch_PressedNo_Higher_Event_Than_FD_Switch_Pressed）：//枚举类型声明mtype = {关闭，打开，清除，选择，武装，活动，未定义，完成，左，右，脱离，锁定，捕获，跟踪};//用于将输入变量值和宏转换为本地//变量{ mtype msg[33]};proctype FGS（chan input_from_otherFGS，input_from_env）{Array2 otherFGS;Array1 env;// FGS状态变量（共82个状态//变量）mtype Onside_FD = Off;bool Onside_FD_On = 0;mtype Modes = Off;input_from_env？env;//模式逻辑if- -！是否_This_Side_Active -> input_from_otherFGS？其他FGS;：：else -> skip;fi;：//对于来自FGS另一端的输入变量值，如果{ mtype msg[13]};proctype env（chan out2fgs，otherinput）{Array 1值; Array 2其他FGS;做：：1->//初始非确定性赋值如果：：1 -> values.msg[0] = On;：：1 -> values.msg[0] =Off; fi;//将一个宏值赋值给对应的//消息字段（类别2）。values.message[26] = When_Turn_FD_Off;if：：1 -> otherFGS.msg[0] = On;：：1 -> otherFGS.msg[0] =Off; fi;- -！Is_This_Side_Active->Onside_FD = otherFGS.msg[0];：：（Onside_FD == Off）When_Turn_FD_On->Onside_FD = On;：：（Onside_FD == On）（env.msg[26]==1）->Onside_FD =关闭;：：else ->skip; fi;Onside_FD_On =（Onside_FD ==On）;如果：：Is_This_Side_Active！= 1->int [1];：：（Modes ==Off）When_Turn_Modes_OnIs_This_Side_Active -> Modes = On;：：（Modes == On）When_Turn_Modes_OffIs_This_Side_Active -> Modes = Off;：：else -> skip;fi;：}：}见图7。 FGS从RSML-e到PROMELA76Y. 崔/理论计算机科学电子笔记133（2005）61宏组1宏组2宏组3宏组4消息传递消息传递环境过程消息自输入消息FGS_正确的过程状态变量历史变量状态转换输入历史变量FGS_左过程状态变量历史变量状态转换输入历史变量见图8。 用于两个FGS通信的4.3基于SPIN的双边FGS模型检验一旦我们成功地使用SPIN对单侧FGS进行模型检查，扩展到双侧FGS就相当简单了。我们创建了两个相同的FGS进程，它们之间的通信通道，而不施加任何同步假设。我们可以直接连接两个FGS进程，使被动FGS可以从其他主动FGS获得实际模式值，而不是让不需要从单侧模型更改FGS过程，并且从env中删除了其他侧FGS值的所有随机值生成和约束。有了这个模型，SPIN使用位状态散列成功验证了相同的属性P1选项;总共消耗了473 M的实际内存。搜索深度已达486220。探索的状态和转变的总数是2。6 × 10 7和3。35×107。相比之下，NuSMV并没有在两个小时内完成使用锥内收敛约简抽象来检查双侧FGS上的相同属性。 不使用抽象，它在几分钟内就占用了内存。我们要注意的是，SPIN验证的结果也是基于部分搜索，其覆盖范围可能非常小。5讨论我们介绍了在商用航空电子规范上使用SPIN的经验，以回答一直困扰我们的问题-符号模型检查器NuSMV或基于显式状态的模型检查器SPIN，哪种工具在可扩展性和可用性方面更适合我们的特定问题领域Y. 崔/理论计算机科学电子笔记133（2005）6177我们的实验表明，在单侧同步FGS模型上，SPIN的性能比NuSMV差，但一旦我们设法处理单侧FGS，SPIN就能更好地扩展到非同步双侧FGS然而，我们不打算强调性能差异，因为有两个主要原因：（1）由于使用位状态哈希选项，使用SPIN的结果可能不可靠，以及（2）性能可能高度依赖于建模者执行的优化级别。我们相信我们的初始优化方法只是一个起点，随着我们对模型检查器的了解加深，可能会有更好的优化。我们也不排除将来通过积极的优化和/或抽象将NuSMV用于双侧FGS的可能性。尽管如此，我们还是从这项研究中得出了三个观察结果;首先，NuSMV在单侧同步FGS上的表现似乎远远好于SPIN。其次，SPIN对于双侧FGS的模型检查是可行的，即使它是通过部分搜索，这是NuSMV不可能的;当系统的大小太大而不能使用exhaustive模型检查时，SPIN可能是更好的选择。第三，SPIN也可以在这个工作中所需的优化是系统的意义上使用，因此可以自动化。 另一方面，有许多问题需要考虑;首先，我们的经验表明，SPIN需要更积极的优化方法才能使其在FGS上工作，并且对模型之间的轻微差异更加敏感。第二，SPIN处理较大系统的能力主要是由于穷举和效率之间的权衡。位状态散列选项允许SPIN执行系统的部分搜索，可能会留下未探索的状态。有几个问题与工具的可用性有关。 在理解SPIN技术和实现的基础上，对系统模型进行模块化和重构，以提高系统的性能。这意味着这些验证工具仍然高度依赖于用户的专业知识。此外，优化的结果可能难以理解。如图7所示，我们已经将宏的名称（旨在提高规范的可读性）更改为无法理解的消息字段名称。这种优化方法可能需要支持，以帮助用户解释优化的系统模型。最后，SPIN支持一次验证一个属性，所有优化方法都需要基于属性。考虑到随着系统的发展，需要在FGS上定期验证298个属性，在最坏的情况下，我们可能需要298个不同的优化模型，每个属性一个。 尽管如此，我们认为，只要我们能够自动化翻译和78Y. 崔/理论计算机科学电子笔记133（2005）61优化过程 我们把这个问题留给未来的调查。引用[1] George S.作者：James C. Corbett和Matthew B.德怀尔对有限状态验证器进行基准测试。Software Tools for Technology Transfer，2（4）：317[2] William Chan，Richard J. Anderson，Paul Beame，Steve Burns，Fracesmary Modugno，DavidNotkin，and John D.里斯大型软件规范的模型检查。 IEEE软件工程学报，24（7）：498[3] 崔云佳和马茨·海姆达尔 模型检查RSML-e需求。 第七届IEEE/IEICE高保证系统工程国际研讨会论文集，第109-118页，2002年10月[4] Edmund M. Clarke，Orna Grumberg，and Doron Peled. 模型检查。 MIT Press，1999.[5] Y. Dong，X. Du，G.J. Holzmann和S.A.斯莫尔卡 在GNU i-protocol中对抗活锁：显式状态模型检查的案例研究。International Journal on Software Tools for Technology Transfer，（4），2003.[6] Y. Dong和X.Du等在i-protocol中对抗活锁：验证工具的比较研究在TACAS会议记录中，1999年。[7] 辛迪·德·纳和多伦·佩莱德。比较软件系统的符号模型检查和显式模型检查。SPIN研讨会，2002年。[8] 题名其余部分：A.同步编程语言：设计，语义，实现。Science of Computer Programming，19（2）：87[9] Dimitra Giannakopoulou，Corina S.帕萨里亚努和霍华德·巴林杰软件组件验证的假设生成。第17届IEEE自动化软件工程国际会议，第3-12页[1