理论计算机科学电子笔记: 软件建模工具的使用研究

理论计算机科学电子笔记164（2006）3-18www.elsevier.com/locate/entcs分析软件建模工具的使用李晓明1、达里尔·香农2、贾巴里·沃克1、萨尔弗拉兹·库尔希德2、达科·马里诺夫11个部门 美国伊利诺伊大学厄巴纳-香槟分校计算机科学系2部门美国德克萨斯大学奥斯汀分校电气计算机工程系xli15@cs.uiuc.edu，dshannon@ece.utexas.edukhurshid@ece.utexas.edu，marinov@cs.uiuc.edujlwalkr1@yahoo.com摘要虽然在改进有助于软件开发的分析和工具方面已经取得了很大进展，但在研究这些工具在实践中如何普遍使用方面却花费了较少的精力。 对工具使用的研究之所以重要，不仅是因为它可以帮助提高工具的可用性，该工具的底层分析技术在一个共同的使用场景。本文介绍了一项研究，探讨（初学者）用户如何使用AlloyAnalyzer，一种用于自动分析Alloy（一阶声明性语言）编写的软件模型的工具。Alloy已经成功地用于研究和教学多年，但还没有研究用户如何与分析仪进行交互。 我们已修改分析器记录它与用户的（一些）交互使用这种改进的分析仪，11名学生在两个研究生班制定了他们的合金模型来解决一个问题集（涉及两个问题，每个问题 一个模型）。我们对结果日志（总共68个分析器会话）的分析显示了几个有趣的观察;基于它们，我们提出了如何提高分析器，分析的性能和用户交互。具体来说，我们表明：（i）用户经常进行连续分析，不同的模型，因此增量分析可以加速交互;（ii）用户关键词：软件建模，合金分析仪，SAT求解器1介绍Alloy [4]是一种一阶声明性语言，适用于表达软件系统的模型。使用合金分析仪[6]，合金模型可以进行全自动分析。分析器使用给定的作用域将Alloy公式转换为命题公式，即，一个宇宙的话语的约束，并使用现成的SAT求解器来寻找具体的例子或合金公式的反例。Alloy已成功用于研究和教学多年，并已协助在各种系统中查找和纠正设计错误[5，7]。然而，到目前为止，还没有关于用户如何与分析器交互的研究学习很重要1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.0014X. Li等人/理论计算机科学电子笔记164（2006）3至少出于以下原因，开发了这样的交互：（1）改进底层分析技术;（2）指出如何使工具更可用;（3）开发用于构建Alloy模型的习惯用法，以实现更有效的分析。Alloy的两个方面使得这样的研究特别值得：语言的声明性和分析器执行的有界穷举检查。一般来说，声明逻辑范式，特别是Alloy，往往会引起连词的普遍使用。Alloy模型通常是通过首先定义表示模型的集合和关系，然后定义适当约束表示的公式来构建的，从最小表示开始，逐步加强它，直到达到足够的细节水平。 以交互方式使用分析器有助于用户进行增量更改并检查其有效性。这些增量变化往往很小，因此分析器可以利用在连续执行1之间引入的差异来使用先前执行的结果提供更快的执行。Alloy的有界穷举检查的性质意味着其结果仅对给定范围有效，即，如果分析器在给定的作用域（范围）内未能找到满足Alloy公式的实例，则实例可能仍然存在于更大的作用域中。对于Alloy用户来说，通过增加范围和重新检查模型来增加他们对模型的信心是很自然的分析器先前未能在较小范围内为其生成期望的实例。请注意，在这种情况下，分析器的两次连续执行之间的模型中的唯一变化是作用域--再次出现了这样一种情况，即分析器可能能够使用前执行。本文介绍了一个研究如何（初学者）用户与合金分析仪。我们已经修改了分析器来记录它与用户的（一些）交互。每次用户编译模型时，修改后的分析器都会保存一个Alloy模型的副本。 为了调查分析器的使用情况，我们要求学生在两个我们（研究生）班的学生解决了一个问题集，该问题集要求他们使用启用日志的分析器开发Alloy模型。我们对来自11名学生的68份日志进行了分析，得出了三个关键结论：(i) 用户经常执行连续执行的模型，只是略有不同，这是预期的基础上，上述两个方面的合金;(ii) 用户与分析仪的交互有时是可预测的，例如， 用户将编译和执行模型，或者用户将要求模型的其他解决方案;(iii) 用户可以自然地开发具有显著不同求解时间的语义等效模型。观察（i）指出，增量约束求解技术可以提高分析器的性能。Alloy1我们使用术语“执行”来指代对Alloy模型的一次检查。通常用于检查的术语是X. Li等人/理论计算机科学电子笔记164（2006）35定量优化合金分析仪。 （二）指出，类似对于连续编译和连续测试[10]，分析器可以在用户编辑模型或视觉检查解决方案时连续地预先计算未来动作的结果。前两个观察结果揭示了如何改进Al-loy工具集。 观察（iii）表明，值得研究Alloy模型的手动和自动转换，这可能会导致执行时间的改善。本文的其余部分组织如下。第2节介绍了与合金分析仪交互的示例。第3节介绍了我们如何从学生与分析器的交互中收集和分析数据。第4节展示了一些初步的结果，提高分析器第五节是论文的2例如接下来我们将说明用户如何与Alloy Analyzer交互，以交互方式开发模型。通过这个例子，我们还介绍了Alloy的一些关键结构。 Alloy的更多细节可在其他地方找到[5]。 作为我们的运行示例，我们使用学生在解决问题集中的问题时与分析器的交互。 这个问题考虑建模的抽象抽象的抽象，CAL结构树，即，一个连通的无环无向图。树有各种（等价的）定义;我们考虑标准教科书中的五个定义[2]。考虑到我们想要在Alloy中对它们进行建模，以便使用分析器检查它们的等效性。在一个典型的场景中，分析器的用户从一个空的模型开始，并在分析器中开发它。然而，为了帮助学生，我们提供了模型的一部分，并要求他们提供其余部分。设G=（V，E）是一个无向图，其中V是一个有限顶点集，E是V上的一个二元关系。以下五个语句是等价的：(i) G是树;(ii) G是连通的，但如果从E中去掉任何边，则得到的图是不连通的;(iii) G是连通的，并且|E|为|V|-1;(iv) G是无环的，并且|E|为|V|-1;(v) G是无圈的，但如果在E上加上任何边，则得到的图有一个圈。Alloy模型由引入基本集合和关系的签名声明以及对这些集合和关系施加约束的公式组成。为了对树建模，我们声明一个sig（即，一组）顶点和该集合上的二元关系来表示边：sigV{//V是顶点集合E：setV}//无向边的二元关系E：V->V基数运算符集声明E是一个任意关系。（运算符one和lone分别声明全函数和部分函数。我们将从顶点u到顶点v的无向边表示为一对有向边（u，v）和（v，u）。因此，在本发明中，6X. Li等人/理论计算机科学电子笔记164（2006）3E是一个对称关系，可以用转置运算符' ~ '表示fact UndirectedGraph {E = ~E}//E是对称的factNonEmpty{ someV}//考虑非空图事实引入了模型的任何实例都必须满足的约束，即，集合和关系的任何令人满意的赋值。事实NonEmpty要求实例至少有一个顶点2。如果表达式e计算为非空集，则公式some e计算为true。（类似地，当e求值为空集时，没有e求值为true我们使用谓词来表达语句1，即，一个可以在其他地方调用的参数化公式：pred Statement1（）{ Connected（）&& 无环（）}pred Connected（）{all disj v1，v2：V| v2中的v1。E } predAcyclic（）{all v：V|（v，E）{predInCycle（v：V，c：V-> V）{v in v. c||somev'：v.c.|设c ' = c -（v -> v'）-（v' -> v）|v' in v.* c ' }所有的oyp r ovides通常的逻辑运算符：&&' '（和），'||’(or),not,‘=>’(implication),and‘<=>’(bi-implication). 关键字disj要求v1和v2是不同的（更准确地说，是不相交的单例集）; all和some分别表示泛量化和存在量化; in表示子集（每个表达式在语义上都是一个集合[5]，因此in不表示集合成员）;'^'表示传递闭包，'*'表示自反传递闭包。v2表达式。因此，E表示沿着E中的边进行一次或多次遍历之后从v2可到达的所有顶点的集合，并且Connected表示任何两个不同的顶点之间存在路径。 谓词InCycle表示顶点v是一个循环的一部分，根据边关系c i，在v处有一个自循环，或者v有一些邻居v '，使得即使我们删除连接v和v'的边，这两个顶点仍然是连接的。运算符' -> '和' - '分别表示配对（更一般地，笛卡尔积）和集合差异。我们的问题集要求学生扩展上述Alloy模型，以表示语句2-5中的每一个。3学生们还必须用Alloy表达五个语句的等价性，并使用Alloy Analyzer进行检查。 接下来我们介绍学生与分析仪之间的交互，以解决上述问题。我们选择这个特定的交互作为用户在使用Alloy Analyzer时通常执行的步骤的代表，通过修改Alloy模型并执行它的循环。用户首先检查提供的模型是否一致：test {！Statement 1（）}检查测试3Alloy断言引入了一个应该检查的公式，在这种情况下，Statement1不成立。命令check指示分析器使用指定的作用域（特别是3）查找给定断言的反例。安-[2]这一条件是声明1-5的等价性所必需的3更准确地说，这道题还要求学生写出谓语Connected。X. Li等人/理论计算机科学电子笔记164（2006）37| |||−Lyzer通过寻找对公式的否定的满意赋值来进行。[4]每个这样的赋值有效地给集合V和关系E赋值，以满足Test的否定（以及隐含的所有事实公式）。当分析器找到一个令人满意的分配时，它可以直观地将其呈现出来（如用户可自定义的图形，其中节点表示特定对象，关系用边表示）。用户还可以选择为给定公式生成更满意的分配。(This分析器中的选项利用了SAT求解器中的解决方案枚举，例如mCha [8]和relsat [1]。用户进一步制定了声明3，并检查了其与声明1的等效性：pred Statement3（）{ Connected（）&&#E = #V-1 } assert Test { Statement1（）<=>Statement3（）} check Test for 3语句3使用集合基数运算符' # '来（错误地）表示定义中的约束E = V 1。合金分析仪为上述公式找到了一个反例。 问题是我们的Alloy模型使用两个有向边来表示每个无向边。 注意，反例不会在一的范围内找到，这将只允许集合V中有一个元素。用户通常从三个或四个范围开始检查：较小的值可能会错过许多反例，而较大的值会导致大量的执行时间。用户很快意识到了错误，并更正了公式：pred Statement3（）{ Connected（）#E= #V + #V- 2}&&这个简单的步骤说明了分析器的强大功能：用户可以自动检查其模型的正确性（在给定的范围内）。快速获取反馈有助于用户在开发模型时对其进行修正。 事实上，正是执行的完全自动化鼓励用户以小步骤和频繁执行的方式交互式地开发模型用户接下来使用check Test for10来检查十范围内的模型。虽然语句1和（已更正）语句3对于最多三个节点的所有图都是等价的，但根据目前的证据，它们对于更大的图可能是不等价的从3到10的范围增加有点不寻常;用户通常会增加1或2的值用户随后添加了声明4：pred EV1（）{ #E = #V + #V-2}pred Statement3（）{ Connected（）EV1（）} pred Statement4（）{ Acyclic（）EV1（）}assert Test { Statement1（）=>Statement3（）&&&&语句3（）=>语句4（）语句4（）=>语句1（）}检查测试4请注意，用户意识到几个语句的等价性可以被排除在外。4除了检查之外，合金分析器还提供了一个命令run，可以直接找到给定公式的满意赋值;runStatement 1for3相当于上面的，可以避免双重否定，但学生可能忘记了命令run。8X. Li等人/理论计算机科学电子笔记164（2006）3用循环暗示的方式来强调5（没有' '或任何其他连接词的行该检查未发现反例，因此用户将范围从4增加到5。然后，用户继续添加语句2和语句5，并在几次检查后得出以下结果：//已连接但删除边会使其断开连接pred Statement 2（）{已连接（）无E或所有v1、v2：V|（v1 -> v2）在E =>设E ' = E -（v1 -> v2）-（v2 ->v1）|一些disj v3，v4：V|不是v4中的v3。E' }pred Statement 5（）{//非循环的但如果添加了任何边，则循环的非循环的（）所有v1、v2：V |E中的not（v1 ->v2）意味着让E ' = E +（v1 -> v2）+（v2 -> v1）|一些v：V| InCycle（v，E '）}assert Test { Statement1（）=>Statement2（）Statement2（）=> Statement3（）Statement3（）=> Statement4（）Statement4（）=> Statement5（）Statement5（）=> Statement1（）}最终模型亦包括上述公式的最新定义使用Berkmin SAT求解器[3]，Alloy Analyzer检查最多4个顶点的所有图的最终断言，并且没有报告反例。SAT求解器在Pentium M 1.8GHz处理器上在4.1秒内完成搜索3研究本节介绍了我们为分析（初学者）用户如何与Alloy Analyzer交互而执行的研究。我们首先描述我们的实验装置。 然后，我们介绍了如何修改分析器以记录其交互。我们接下来讨论分析结果日志。我们最终表明，等价的Alloy模型可能需要显著不同的求解时间。3.1实验装置我们收集了德克萨斯大学奥斯汀分校和伊利诺伊大学厄巴纳-香槟分校的研究生在两个研究生研讨会学生们在上课前没有合金的经验，但大约有两个半的合金讲座。这套习题包括两个问题。一个问题是我们正在运行的关于树定义建模和检查它们的等价性的示例另一个问题是建模并解决一个用英语给出的难题[14]，将八个不同的工作分配给四个受约束的人。我们告诉学生如何使分析器能够收集他们的模型开发的日志。我们还告诉他们，我们可能会使用他们开发的（匿名）模型作为案例研究，调查用户如何使用分析器，以及如何开发增量技术来提供更快的解决方案。我们没有[5]这也是教科书中证明等价性的方法X. Li等人/理论计算机科学电子笔记164（2006）39告诉学生我们想做的具体实验。 提交日志的记录是自愿的，并没有影响学生的成绩，无论是积极的还是消极的。他们的解决方案只根据他们发送的最终模型进行评分。3.2测井我们设计日志工具是为了向Alloy开发人员提供使用数据，这些数据可能有助于进一步改进Alloy工具集。当前日志记录工具记录编译、执行和用户界面事件。回放事件所需的所有信息都被存储，以及记录事件开始和结束时间的时间戳。除了时间戳，存储的信息还包括Alloy Analyzer和SAT求解器的配置、正在编译的源文件（以及引用的任何源文件）以及命令的字符串表示。本文主要关注两种类型的事件：（1）编译，记录用户如何编译模型，以及（2）执行，记录用户在成功编译后如何执行命令。虽然本文只使用了两种类型的事件，但我们的日志记录工具记录了其他使用数据，这些数据可能会进一步提高对Alloy Analyzer使用模式的理解。 例如，用户界面事件可以帮助简化分析器的工作流程3.3分析接下来，我们将对这两个类中收集的日志进行分析。 我们总共收集了11名学生的日志。(Many学生们要么在网上工作，要么错误地使用日志，因此没有为我们提供有用的日志。） 一共有68次UI会话和2308次编译。在这些编译中，391个（或16.9%）由于编译错误而失败，452个（或19.5%）是成功的编译，但没有任何执行。不幸的是，我们的日志没有记录失败编译的模型，因为我们没有期望它们对改进Alloy Analyzer有用。然而，他们相对较大的百分比表明初学者用户可能在学习Alloy的某些构造时遇到问题。我们计划在未来记录失败的模型;分析它们以确定语言或其文档中的潜在改进以避免常见错误将是有趣的。显然，用户很快就学会了如何处理编译错误：用户开始更频繁地编译模型，以便在模型的最近更改部分接下来，我们分析1465个记录的成功编译和执行，以检测用户在连续执行之间对模型进行了哪些更改。我们把变化称为事件。我们首先介绍我们的分析检测到的事件类型。然后，我们描述了我们的分析如何检测这些事件使用的语法和语义比较的水平。（这些不是完整的句法和语义比较，稍后会解释最后，我们给出了分析结果。10X. Li等人/理论计算机科学电子笔记164（2006）33.3.1事件回想一下，Alloy模型由签名（对应于程序中的数据）、公式（对应于程序中的代码）和命令（对应于程序运行中的输入）组成。该命令的一个重要部分是指定作用域，即，模型中基本集合的边界。我们定义以下事件来跟踪模型各部分的变化• 对于签名：SN（sig new）添加新的sig; SD（sig delete）删除sig; SM（sig mod）修改现有的sig。• 对于公式：FN（公式新建）添加新公式; FD（公式删除）删除公式; FM（公式修改）修改现有公式。• 对于命令：CN（命令新建）添加新命令; CD（命令删除）删除命令; CM（命令mod）修改现有命令。• 对于范围：OS（仅范围），模型中的唯一更改是范围的更改在命令中; ND（非递减）范围仅增加; OO（一个一个）仅增加一个界限，正好是一个。• 事件摘要：SS（单签名）模型中仅更改了一个签名; SF（单公式）模型中仅更改了一个公式; CR（连续重复）两个连续执行具有相同的签名、公式、命令和范围; ER（执行重复）重复执行，但不一定是连续执行。我们已经编写了一个程序，它遍历给定的日志（或一组日志）并计算事件的数量。程序如下进行。它首先从模型中删除语义上不必要的语法元素，如注释和空格。然后，它解析模型的一部分，并使用两种类型的比较：语法比较（针对SN、SD、SM、FN、FD、FM、CN、CD、CM、SS和SF事件）和语义比较（针对OS、ND、OO、CR和ER事件）。3.3.2句法比较我们程序中的句法比较使用了文本相似度的概念。程序将每个语义单元（签名、公式、命令）分成两部分：单元的声明和单元的内容。 程序将分别比较这些单位。例如，以下符号定义：一个sigV扩展 W{ E：set V}表示为3元素元组（V，E：setV，one，extendsW），其中one和extends是分别指定单例集和子集的Alloy关键字。然后，两个签名的相似性是三个分量的相似性的加权和;我们当前的实现对这三个分量使用相等的权重我们的程序使用编辑距离[9，12]作为两个组件字符串之间相似性的度量。两个字符串之间的编辑距离是将一个字符串更改为另一个字符串所需的重复次数。我们使用编辑距离X. Li等人/理论计算机科学电子笔记164（2006）311因为我们的目标是找出用户在连续执行之间改变了什么。编辑距离被标准化为两个字符串的长度。 当编辑距离为0时，表示两个字符串相同。 当编辑距离为1时，表示这两个字符串是完全不同的。0到1之间的值表示两个字符串的相似性。编辑距离越小，相似度越高。 例如，当编辑距离为0.5时，我们需要更改一个字符串的50%才能获得另一个字符串。句法比较的一个优点是，它比语义比较更能追踪某些变化。例如，如果用户将定义从sigV更改为一个sigV，则两个版本的内部Alloy表示非常不同，而语法比较可以很容易地发现用户只更改了一个sig定义。然而，语法比较的局限性在于，当需要更小粒度的差异时，它需要进一步解析，例如检测命令中是否仅范围发生了变化我们可以根据两个语义单位的成分之间的相似性，将它们定义为相等的、修改的或不同的。如果两个语义单元之间的编辑距离为0，则它们相等。 我们的程序使用一个经验选择的阈值25%，以确定两个单元是修改版本还是只是不同。(We通过对几个随机选择的示例进行详细的手动比较检查来确定阈值。 如果编辑距离低于阈值，则将单位视为修改后的版本。否则，它们是不同的。我们的阈值相当高，因此将两个版本视为修改版本的置信度很高，也就是说，这两个版本只有很小的差别。 换句话说，数据显示图1中的结果略微低估了修改案例的真实数量，因此低估了增量求解可以为合金分析仪带来的潜力3.3.3语义比较我们程序中的语义比较解析模型，并执行一定程度的语义分析，以检测用户所做的更改。具体来说，我们的程序根据作用域检测每个基本签名的边界。我们的树的运行示例只有一个签名V，但通常在模型中可以有多个签名。然后，范围是这些签名中的每个签名的边界的向量。用户可以在命令中以多种方式指定范围。完整的细节在其他地方[5]，我们在这里只提供了几个例子：对于5个指定检查Eq，所有签名的边界应该是5，对于4个V指定检查Eq，V应该绑定4，而其他签名应该具有默认值（当前为3），检查Eq5但3个V指定除了V应该是3之外，所有签名都应该绑定5。我们的程序分析命令和签名来构建整个作用域向量。然后比较Alloy模型的不同执行之间的这些范围向量。3.3.4事件数量图1显示了用户在更改Alloy模型时执行的事件数量。对于编译次数最多的19个UI会话中的每一个，我们将12X. Li等人/理论计算机科学电子笔记164（2006）3ses。SNSDSMFNFDFMCNCDCMSS1000197502018230200022218914030001134141130400000187750500000191013110600100340001700010232220080002035821209783251735541631000000486610011000214266180120001035992001300001219960140003225423015000002910170168130322229149120170001038003018282112585515219191183115177744总和3640141317061113511921210ses。SFOSNDOOCR儿#C147171253149222313944165032554118484184421535519865164363466069417184410436819540243993810621360104295000571136181251163122818136235713204211134142842016341525121060043163255037521726870243718579602207619276600042总和5621651233831111939图1.一、用户在19个UI会话期间修改模型时执行的更改事件数执行的事件总数。在59.9%（562/939）的情况下，两次连续执行之间的修改仅涉及一个公式，17.6%（165/939）的连续执行仅在其范围内不同。 这些数字突出了合金分析仪中增量求解的重要性。此外，所有模型执行中有11.8%（111/939）与同一UI会话中的某些先前执行相同。（虽然类似的连续模型类似于空间局部性，但重复模型类似于时间局部性。这表明分析器可以缓存执行结果，并将每个新模型与先前执行的模型进行比较。X. Li等人/理论计算机科学电子笔记164（2006）313≤≤3.4等效型号，不同性能接下来，我们证明语义等价但语法不同的Alloy模型可能需要显著不同的求解时间。虽然很明显（几乎）任何推理系统的解决时间取决于问题的具体公式，我们的结果表明，初学者Alloy用户自然会创建需要不同解决时间的模型。因此，我们的结果提供了证据，对沙利文等人的索赔。[11][第140页]：因为TestEra使用了Alloy Analyzer虽然可以人为地构建具有不同求解时间的等效Alloy模型，但我们将学生实际提交的模型视为问题集的解决方案。具体地说，我们考虑为树等价问题提交的解决方案，用作我们的运行示例。回想一下，这个问题要求学生对树的五个定义进行建模并表达它们的等价性。当学生们想出几个不同的公式来表达定义时，他们也想出了五个不同的公式。来表达等价性。这让我们非常惊讶，因为我们预计学生可能只使用两个或三个公式来表达等价。这种多样性表明，学生们可能没有复制解决方案。 更严重的是，这种多样性表明，新手用户可以以一种意想不到的方式使用工具，从而使专家用户（甚至是工具开发人员）感到惊讶。最后，多样性为了解用户如何使用合金分析仪提供了额外的动力。为了展示学生们检验等价性的方法，我们使用Si代表语句i（），其中1 i 5。学生们使用四个不同的公式进行等效：断言等式1{ S1 => S2 S2 => S3 S3 => S4 S4 => S5 S5 => S1}断言等式2 { S1 => S2S1 => S3S1 => S4S1 => S5}断言等式3{ S1 => S2 S2 => S3 S3 => S4 S4 => S5 S5 => S1}断言等式4 { S1 => S2 S1 => S3 S1 => S4 S1 => S5 S2 => S3 S2 => S4 S2 => S5&&S3 => S4S3 => S5一个学生使用了一种相当不同的方法来检查等价性;而不是在一个公式中表示所有语句的等价性，学生使用了四个公式：//一次取消一行注释以检查等价性。//assertEq5 { S1 => S2}//assertEq5 { S1 => S3}//assertEq5 { S1 => S4 }assertEq5 {S1 => S5}接下来，我们比较分析器的性能，以检查上述等效性。还要注意，所有这些断言在它们之间是等价的;事实上，它们都等价于true。 因此，否定的断言是不能令人满意的，分析者不能找到任何解决方案的否定（和反例的我们将每个断言与14X. Li等人/理论计算机科学电子笔记164（2006）3相同的模型来表达树定义，并检查范围的断言四口对于等式5，我们分别检查所有四个断言并对所有四次求和。检查示波器4，合金分析仪需要12.6秒进行等式1，10.7秒对于等式2，16.2秒对于等式3，28.6秒对于等式4，以及20.1秒对于（所有四个）等式5.因此，最好的配方在求解时间上比最差的配方加速2.67倍。当我们检查范围5的相同断言时，速度增加到5.75倍。这一结果指出，用户应该意识到，不同的模型可以导致非常不同的解决时间。实际上，专家Alloy用户通过经验获得了这一点，并重写了他们的模型以加快执行速度。我们把它作为一个未来的工作，研究这些重写，以产生一套准则用于（重新）编写模型以获得有效的执行。4潜在改进本节显示了一些初步结果，说明了改善合金分析仪性能的潜力。我们提出了两种类型的改进：（i）可以通过使用增量SAT求解来加速（类似）连续模型的执行来获得的改进，以及（ii）可以通过在用户编辑模型或视觉检查解决方案时计算一些结果来获得的改进。4.1增量求解如前所示，Alloy用户经常一个接一个地执行类似的模型。这使我们考虑使用增量SAT求解器来改善分析器的执行时间。增量SAT求解器的工作原理如下[13]。他们首先采取一个SAT问题，像往常一样，并确定它是否令人满意。此外，它们还跟踪它们执行的推理步骤如何依赖于输入子句。之后，下一个SAT问题可以呈现给求解器，而不是从头开始，作为前一个SAT问题的增量，它描述了要删除哪些旧子句和要添加哪些新子句。求解器然后可以使用此信息来使依赖于删除的子句的推理步骤无效，并仅对新子句执行搜索。与从头开始求解新问题的SAT求解时间相比，只求解delta通常会大大缩短SAT求解时间。我们提出的结果，利用增量SAT解决在两个步骤中进行的合金分析仪：（i）只添加一个事实的模型和（ii）增加瞄准镜的精确度是1这些只是评估增量执行潜力的初步结果。为了获得准确的结果，我们需要修改整个分析器来执行增量执行。4.1.1添加事实Alloy用户可以通过添加新的事实来为他们的模型添加约束。 用户可以在构建模型或调整实例生成时添加事实（或X. Li等人/理论计算机科学电子笔记164（2006）3152.2增量编译21.81.61.41.210 246例8 10图二、加速连续模型的增量执行，这些模型只在一个事实之外发生反例）。例如，回想一下第2节中的以下断言：test {！Statement 1（）}检查测试3分析器的执行生成一个只有一个顶点没有边的树。 假设 我们想要看到更大的树，比如说一棵树只有两个顶点。 我们 可以添加以下事实来表达这一要求：事实目前重新运行分析器需要转换修改后的Alloy模型将其整体转化为CNF公式，然后求解该公式。相反，使用增量SAT求解器，我们可以简单地使用增量转换为求解器提供增量，增量转换仅产生表示新约束的布尔公式。这样做不仅允许求解器更有效地生成所需的树，而且还消除了将整个Alloy模型转换为CNF的需要。 在我们的实验中，我们修改了Alloy编译器，以便编译器可以将delta事实转换为delta布尔公式。通过对两个连续模型的比较，我们可以发现后一个模型中的新事实。我们修改后的编译器重命名了这个事实，使得原来的Alloy编译器只为新的事实生成CNF公式。我们的修改器编译器还指示SAT求解器重用先前模型的求解轨迹。在生成delta布尔公式时，保持先前模型和布尔变量之间的转换，以便用户可以可视化新事实如何影响原始解决方案。我们的修改确保了delta解决方案的正确性，即，我们通过重用以前的解决方案来提高性能，但新的解决方案既满足了有无delta事实的模型图2显示了使用我们的增量编译的性能增益。我们从日志中提出了10种情况，其中用户在两个连续执行之间只向模型添加一个事实这10种情况对原始模型有显著的求解时间，因此可以观察到速度的提高;如果原始模型的求解时间很短，我们就不需要增量求解。我们测量求解原始模型的时间（torig），用增量事实整体求解后一个模型的时间（torig+delta），以及增量求解后一个模型的时间，即，加速比16X. Li等人/理论计算机科学电子笔记164（2006）3不tdelta+torig−≤仅求解delta事实（tdelta）。加速由torig+delta+torig给出。增量编译的加速范围为1.03 - 2.04倍，平均为1.56倍。请注意，我们在两种情况下都考虑了两次执行的时间总和;第二次执行的加速是torig+delta，甚至更高。三角洲4.1.2扩大范围增量求解不需要只使用增量SAT求解器来执行。 分析器考虑用分析器检查断言。如果找不到反例，Alloy用户可能会通过增加范围和重新执行分析器来提高他们对模型的信心，如以下学生日志中的连续执行所(i) 检查测试4(ii) 检查测试5由于Alloy如果分析器未能使用范围i找到反例，则当用户在对范围i执行相同检查之后对范围i执行检查时，范围j i）不存在反例1我们可以使用在第一次执行期间没有找到反例的事实来指导分析器检查正好i个顶点。 为了说明，检查的时间 第2节中范围5的等效公式从8分43秒缩短为8分24秒 虽然在这种情况下，改善仅为3.5%，但我们认为，更好的技术可以产生更高的加速。日志显示，所有执行中有17.6%（165/939）只增加了作用域。其中，23.0%（38/165）的命令仅在一个签名上增加一个范围。数据表明，用户经常增加范围，通常是小步。因此，增加范围的增量求解可能会提高合金分析仪的性能4.2连续执行连续编译是一种减少集成开发环境中延迟时间的方法：当程序员编辑程序时，机器在后台编译程序，因此当程序员需要时，要执行程序，它已经编译好了。最近有人提出了一种类似的技术来进行测试。 持续测试[10]在程序员编辑程序时在后台运行单元测试;如果测试失败，程序员会被警告他最近的更改可能会破坏一些回归测试。我们建议在Alloy Analyzer中使用类似的方法：它可以连续执行模型，以准备用户（可能）下一步要求的结果。这自然适用的一种情况是当用户正在编辑模型时。然后分析器可以将模型转换为SAT，并在基础SAT求解器上运行它。在询问解决方案后，用户将看到X. Li等人/理论计算机科学电子笔记164（2006）317−它更快。 另一个有点令人惊讶的情况是，当用户正在目视检查模型的一个解决方案时，连续求解适用：分析器可以指示SAT求解器在后台生成下一个解决方案。我们的研究结果表明，（初学者）用户不太可能检查下一个解决方案，但如果他们检查下一个解决方案，他们往往会重复此操作连续几次反复查看下一个解决方案是我们在专家Alloy用户中观察到的轶事。接下来，我们提出的结果，估计减少的延迟获得下一个解决方案，并没有连续执行。我们无法获得精确的结果，因为我们的日志没有记录用户与Alloy Analyzer的整个交互，因此我们不知道用户执行所有操作的精确时间。我们的日志记录了用户何时开始检查下一个解决方案以及SAT求解器何时返回结果。 我们用begini来表示第i次检查，并在将结果返回给用户时结束i因此，开始i+1endi是用户检查第i个解决方案的时间段，如果我们可以将第i+1个解决方案的计算和用户检查重叠，则获得第i +1个解决方案的延迟也可能减少我们检查了84个案例，其中用户在日志中检查下一个解决方案。平均而言，用户花费8秒检查返回的解决方案，等待SAT求解器返回下一个解决方案的时间不到1秒。在所有84种情况下，用户花在目视检查上的时间比SAT求解器生成下一个解决方案所花的时间要长。如果分析器指示SAT求解器在返回前一个解之后立即搜索下一个解，则用户可以在需要下一个解时立即获得下一个解。5结论和今后的工作我们分析了Alloy Analyzer的使用情况，这是一种自动检查用Alloy（一种一阶声明性语言）编写的软件模型的工具。虽然之前已经有很多关于Alloy的工作，但还没有研究用户如何与分析器交互。我们分析了11名研究生在为一个问题集开发两个模型时与该工具的交互。我们的研究结果表明：（i）用户经常使用稍微不同的模型执行连续的执行，因此增量检查可以加速交互;（ii）用户与分析器的交互有时是可预测的，并且分析器可以在用户编辑模型时预先计算未来动作的结果;（iii）（初学者）用户可以自然地开发语义上等价的模型，但执行时间却明显不同，因此值得研究可以改善执行时间的我们的结果为合金分析仪的进一步分析提供了一个令人鼓舞的起点。我们计划收集更多日志并进行分析，以检测分析器的潜在进一步改进。在分析器中实现完整的增量执行和连续执行将是18X. Li等人/理论计算机科学电子笔记164（2006）3实现潜在的改进。更一般地说，Alloy Analyzer只是软件开发中使用的一个示例工具。我们认为，研究工具的使用是重要的，我们计划在未来探索其他工具的使用。致谢我们要感谢我们班的11名学生提交了他们与合金分析仪交互的日志。我们还要感谢匿名评论者对本文前一版本的评论。 我们感谢 感谢德里克·雷赛德和格雷格·丹尼斯对合金测井的帮助引用[1] 小巴亚多R. J.和R. C. Schrag，使用CSP回看技术来解决现实世界的SAT实例，在：国家人工智能会议论文集，1997年，pp.203-208[2] Cormen，T. H、C. E. Leiserson和R. L. Rivest，[3] Goldberg，E.和Y. Novikov，BerkMin：A fast and robust SAT