没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记190(2007)3-18www.elsevier.com/locate/entcs翻译一个,分析多个:利用Microsoft中间语言和源代码转换进行模型检查Jesse McGeachie1 Juergen Dingel2加拿大金斯顿皇后大学计算机学院摘要在本文中,我们提出了一个基于源代码转换的框架,以支持模型检查的源代码编写的语言属于微软的.NET平台。该框架包括一组指导转换的源转换规则、支持断言检查的工具以及用于死锁检测自动化的工具。该框架产生了可执行的和形式上可验证的工件。我们提供了框架中的工具的细节,并评估了一些小的案例研究的框架。关键词:源代码转换,模型检查,TXL,微软中间语言,Java字节码。1引言近年来,软件开发已经看到了各种新兴技术和编程语言。微软C#、VB .NET、J#)正在经历越来越多的流行。微软中间语言(MSIL)[9]构成了.NET的核心,所有属于.NET的语言都编译到它上面。 在MSIL的帮助下,.NET将Java的“一次编写,到处运行”概念推广为“多次编写,到处运行”。近年来,软件模型检测技术是一个非常活跃的研究课题.已经提出了许多旨在实现两个目标的技术一是1 电子邮件:jesse. gmail.com2 电子邮件地址:dingel@cs.queensu.ca1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2007.02.0574J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3全自动的、高度优化的、但详尽的状态空间探索的好处应该被用于用标准的高级语言(如Java、C/C++或C#)编写的程序。其次,应避免将程序容易出错的手动翻译为已建立的模型检查器(如Spin [6]和SMV [2])的输入语言的陷阱。随着日常软件中越来越多的并发趋势(例如,为了获得性能优势[17]或实现嵌入式系统),这项研究似乎特别及时。现有的软件模型检查器或者将程序翻译成现有模型检查器的输入语言(例如,Bandera [3],或Feaver [7]),或增强语言的执行环境以执行模型检查(例如,[18]或[19]或[19]。在本文中,我们研究了一个软件模型检查器的. NET的发展。更确切地说,我们展示了如何利用像MSIL这样的通用表示来进行一般的分析,特别是模型检查。原则上,MSIL允许仅通过一个转换来分析多种语言这项工作的贡献是一个框架(MSILCAD),用于将MSIL的子集自动转换为Bandera中间表示(BIR),Bogor模型检查器的输入语言[15]。在我们的框架的核心是微软中间存储到Java字节码转换(MSIL2JBC)。MSIL2JBC转换旨在支持MSIL的一个子集,该子集是C#和J#编程语言的一个合理大小的子集的结果。该框架还包含支持断言冲突检查和死锁检测的工具。据我们所知,MSIL的唯一其他模型检查器是Zing [1]。与Zing相比,我们的框架是基于预防的,并利用了Bandera工具集的功能。我们选择使用TXL [4]实现MSIL2JBC翻译,TXL是一种专门设计用于支持结构源转换的编程语言。负责MSIL2JBC转换的TXL程序将许多转换规则应用于MSIL输入,这些规则被分成规则集,每个规则集都有自己特定的转换目的。例如,一个规则集处理线程的创建,而另一个规则集提供支持方法调用的能力,等等。在本文的其余部分,我们将在第2节提供MSIL、Java汇编格式JASMIN [11]、TXL和Bandera的背景第4节解释了MSILCAD的评价和示例实验,第5节讨论了相关工作。最后,在第6节中给出了结论,随后是未来的工作。2背景2.1Microsoft中间语言微软.NET平台的核心它类似于Java字节码,J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)35更复杂,因为它是专门设计为许多语言的目标源代码在被即时编译为某个目标平台的本机代码之前,先被编译为这种中间语言。本文中介绍的工作只关注这种语言的一个有限子集,本节的其余部分将只关注该子集。MSIL是一种基于堆栈的语言。 我们关注的MSIL的子集包含将文字值加载到堆栈(ldc),创建数组(newarr),在字段之间加载和存储值(ldfld,ldsfld,stfld,stsfld),加载方法参数(ldarg)以及其他一些指令。支持处理标准算术和布尔比较的指令此外,什么都不做(nop),有条件地(br)或无条件地(brfalse,brtrue)分支,以及从方法返回(ret)的指令也被处理。最后,通过允许线程和监视器,对象转换仅限于作为C#和J#源代码子集结果的MSIL代码子集,不包括C#中可能存在的任何不安全代码(非托管指针)。2.2JasminJava程序的Java字节码驻留在程序的类文件中。它是二进制格式的,因此不容易操作。通过使用Sun Microsystems提供的javap反汇编程序,可以生成ASCII字节码指令对于反向(ASCII到JBC),Sun没有定义标准的Java汇编程序格式,因此不存在从ASCII格式的字节码汇编Java程序的标准工具JASMIN [11]是一个Java汇编接口,它接受Java类的ASCII描述,使用Java虚拟机[10]指令集以简单的汇编类语法编写,自创建以来,JASMIN已成为Java事实上的标准汇编格式。我们的工作使用JASMIN语法作为转换的目标语言,这样我们就可以利用JASMIN汇编器来生成Java二进制文件。2.3使用TXL进行源代码转换TXL [4]是一种专门设计用于支持源代码转换的编程语言。TXL支持统一化、深度模式匹配和隐含迭代,并结合了函数式和基于规则的编程功能。TXL程序由两部分组成:一个上下文无关的,可能是模糊的语法标记,它描述了要转换的工件的整体语法结构,以及一组结构转换函数和规则,它们使用模式替换对来描述所需的转换。TXL的实现和形式语义基于树重写,其中匹配的转换规则应用于输入,直到达到固定点。例如,当在包含数字序列的文件上调用时,TXL程序6J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3定义输入[重复数]结束定义规则主替换[重复编号]N1 [数量] N2 [数量]剩余[重复数量]哪里N1 [>N2]通过N2 N1静止结束规则Fig. 1. TXL程序对文件中的数字进行排序在图1中,对文件的内容进行了排序初始定义语句表示程序的输入可能是一个空的数字序列,其中“number”是一个内置的非终结符,它匹配任何以数字开头的规则匹配每对输入中的连续数n1和n2是无序的,并将该对替换为n2和n1。只要可以匹配,就会应用该规则。如果找不到任何规则的匹配,则TXL程序终止。2.4班德拉Bandera是一个基于组件的模型提取器和Java程序的模型检查器。它当前的实现处理所有Java,包括对象同步、多线程和断言。其基于组件的模型提取体系结构的设计,可扩展性,可伸缩性和可扩展性。我们的框架利用Bandera从Java代码中提取优化模型,并对这些模型进行断言违规和死锁的模型3MSILCAD概述MSILCAD(MSIL检查断言死锁)的整体架构如图2所示。用户使用一个显式输入调用MSILCAD:要翻译和分析的C#或J#源代码。源代码首先由预转换处理器处理,这确保源代码中的断言由MSIL2JBC转换器正确处理修改后的源代码是J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)37转换前处理JBCMSIL至JBC翻译源代码BIR模型图二. MSILCAD体系结构概述然后反汇编为MSIL代码,并直接传递给MSIL2JBC转换器。MSIL2JBC转换器生成Java字节码和Java源代码,两者都对应于转换器传递的MSIL代码。最后,Java字节码和源代码被传递到转换后处理器,在那里Bandera准备分析,断言代码被最终化,从Java源代码中提取BIR模型,Bandera用于检查断言违规和死锁。MSILCAD的所有步骤的详细信息在本节的其余部分中给出3.1预转换处理器预转换处理器体系结构的概述如图3所示。源代码修改源代码MSIL代码图3.第三章。转型前处理器体系结构概述3.1.1断言预处理器。MSIL2JBC转换器不处理字节码级别的断言使用,因为在从字节码进行汇编的过程中,断言预处理器将源代码中的断言替换为MSIL2JBC能够翻译的内容,以便标记它以供以后发现。然后,在转换后处理阶段,定位这些替换并实现断言。这一步是用一个简单的Visual Basic脚本实现的。3.1.2源代码编辑器。修改后的C#或J#源代码然后用各自的编译器编译,产生可执行的二进制文件。这一步是必要的,因为拆卸MSIL转换后处理断言预处理器编译二进制源编译器IL反汇编程序8J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3TXL规则细分6方法范围规则441431见图4。 TXL规则集层次结构MSIL代码需要二进制作为输入。3.1.3中间语言反汇编程序。IL反汇编器将编译器生成的二进制程序作为输入,使用Visual Studio.NET提供的ildasm实用程序对其进行反汇编,从而生成与原始C#或J#源代码对应的ASCII格式的MSIL代码。3.2MSIL到JBC转换本节描述完成MSIL到JASMIN源代码转换的TXL程序。翻译已被分解为18个单独的规则集,服务于个人的转换目的,共有144条规则。有些规则集是完全独立于所有其他规则集的,而另一些则非常依赖于它们之前的规则集的结果来实现它们的目的。图4示出了规则集的集合的层次结构,以及每个集合中的规则的数量。规则集必须应用于所示的层次结构,以确保翻译的正确性。由于篇幅限制,下面只讨论最有趣的规则集。3.2.1TXL转换。J#全局预处理器规则集:我们没有创建专门为J#设计的一整套新的转换规则,而是为我们最初支持的C#子集确定了J#和C# MSIL代码之间的差异,并创建了一些将J# MSIL转换为等效C# MSIL的规则。更具体地说,这组规则用于删除不必要的J#MSIL,并对方法和类头进行微小的调整,以满足C# MSIL的语法。通过利用我们现有的MSIL2JBC转换规则,J#全局预处理器规则集方法范围规则方法头规则集线程标识规则集类头规则集J#全局后处理器规则集文件输出规则集15J#方法预处理器规则集3比较规则集15分支规则集8映射规则集19对象同步规则集附加方法转换规则集10其他化妆品11规则集对象创建和处理规则集1944加载指令规则集剩余指令规则集2例外表规则集2J#方法后处理器规则集J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)39对J#的支持非常重要。方法标题规则集:方法标题规则集有三个重要任务:(i) 将MSIL方法头转换为等效的JASMIN头。(ii) 翻译方法头中的方法参数以及任何其他上下文。(iii) 翻译方法头以及任何其他上下文中的类型声明对 于 转 换 类 型 声 明 , 使 用 带 有 静 态 映 射 表 的 TXL 规 则 图 5 展 示 了 规 则 cconvertTypes。静态映射表存储在typePairs构造中。表中最左边的列表示MSIL中的类型声明列表示相应的JASMIN类型声明。该规则匹配MSIL中的所有类型声明,在此表中执行查找,并将MSIL类型声明替换为正确的JASMIN声明。例 如 ,如果类[mscorlib] System.Threading.Thread匹配,则它将被替换Ljava/lang/Thread;线程识别规则集:此规则集的目的是定位MSIL代码中的线程,并将这些线程转换为语义等效的JASMIN代码。线程在C#中比在Java中更容易实现,这导致了不平凡的转换。为了减轻这种转换的一些固有困难,允许使用线程的方式受到限制:旨在作为单独线程运行的代码必须包含在与任何其他线程不同的单独类中,并且仅允许包含main方法的单独类实例化任何新的Thread对象。注意这通过对源代码的一些操作,限制总是可能的。类头规则集:类头规则集将所有MSIL类头和类字段声明转换为等效的JASMIN。这些转换相对简单,因为MSIL和JASMIN之间的差异很小:描述类的信息是以不同的顺序,MSIL包含的类信息在JASMIN中没有意义,这意味着它是.NET架构特有的。JASMIN比较规则集:JASMIN比较规则集将用于比较整数值(ceq、clt、cgt)的三条MSIL指令转换为等效的JASMIN指令。表1举例说明了其中一种翻译。ceq指令比较两个整数值n1和n2,如果n1等于n2,则将1压入堆栈,否则压入0。没有一条JASMIN指令与此功能等效,因此,需要指令来模拟这种精确的行为。10J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3规则c convertTypesconstruct typePairs [重复类型对]’int8 ’I ’int16 ’I ’int32’I ’int64 ’I’int8 ’[’]’int16 ’[’]’int32 ’[’]’int64 ’[’]’bool ’Z ’bool ’[’]’class ’[ ’mscorlib ’] ’System.Threading.Thread ’Ljava/lang/Thread; ’class ’[ ’mscorlib ’] ’System.Threading.Thread ’[’]替换[类型]deconstruct * [typeMatches] argMemoryanytype [type]deconstruct * [type pair] typePairsanytype corr [type]通过Corr结束规则图五. 类型声明映射规则集:由于MSIL和Java字节码以不同的方式处理数据的存储和访问,因此必须跟踪方法的参数和局部变量。MSIL必须从两个不同的存储位置访问参数和变量,而Java字节码只需要访问单个位置。这导致MSIL需要两个不同的指令来访问这些位置(ldarg,ldloc),而JASMIN只需要一个。 而且任何给定参数或变量在存储位置中的位置都将发生变化J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)311表1ceq指令翻译MSILJBCCEQifeq BRANCH 1iconst 0转到BRANCH 2BRANCH 1:iconst 1第二分部:表2局部变量和参数加载指令的动态表局部变量动态表参数动态表00009990001 –2 –在MSIL和JASMIN之间更复杂的是,用于存储和加载到数据存储位置以及从数据存储位置加载的JASMIN指令需要一个前缀,表示存储或加载的数据类型。MSIL指令不需要此类信息。映射规则集动态创建一个表,该表将用于加载和存储的MSIL指令与等效的JASMIN指令相匹配,并完成匹配的索引和类型前缀。 动态表然后在任何时候在其他规则集内被引用,以便产生用于加载和存储指令的正确翻译。这个动态表看起来类似于前面图5中提到的静态表,但是必须动态创建,因为在编译时存储在其中的信息是未知的。表2说明了用于加载指令的局部变量和参数动态表的典型示例。每个表中的第一个条目只是表示一个占位符,以满足TXL语法要求。加载变量动态表中的第二个条目指出,局部变量存储位置中的位置0应映射为类型integer(iprefix),并映射到JBC中的位置1(1summix)。来自同一表的最后一个条目被标记为位置999,并且用于表示存储异常对象。异常对象是引用类型,所以load指令前面加了a,表示引用类型。参数动态表(ADT)也可以类似地解释。每个表都位于一个全局变量中,并根据需要由许多TXL规则导入和使用 图6说 明 了 c loadArgumentsTXL 规 则 如 何 使 用 来 自 Load Instructions Rule-set 的ADT。12J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3rule c loadArgumentsimport argMemory [重复类型匹配]replace [methodBodyItem]该死 整数[deconstruct * [typeMatches]argMemorysomenumber'- > corrInstLOAD[methodBodyItem]通过corrInstLOAD结束规则见图6。 c loadArgumentsTXL规则具有某个位置值(somenumber)的ldarg指令由规则匹配,位置值被提取并在ADT(argMemory)中的查找期间使用,并且对应的MSIL指令(corrInstLOAD)从表返回并在替换中使用监视器规则集:监视器规则集提供对对象同步使用的支持。更具体地说,支持.NET Monitor类中的以下方法:Enter、Exit、Wait、Pulse和PulseAll。异常表规则集:转换期间发现的异常存储在动态全局变量中。 在翻译结束时,最终的异常表被添加到JASMIN代码中。3.2.2 JASMIN大会。在完成MSIL到JASMIN的源代码转换之后,JASMIN源代码文件立即被组装成二进制格式的实际Java字节码,也称为Java类文件。3.2.3JAD反编译。最后,Java类文件使用一个名为JAD的支持命令行的Java反编译器进行反编译[8]。反编译类文件的结果是Java源代码。3.3转换后处理器图7展示了转换后处理器的总体架构。J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)313最终会话文件会话文件Java源Java源代码修改源代码分析模板代码输出图7.第一次会议。转换后处理器体系结构概述3.3.1Bandera预处理器。Bandera需要三个输入:Java源代码、Java字节码和Bandera会话文件。Bandera需要一个会话文件来通知自己源代码和字节码在主机上的位置,以及所涉及的哪些类包含主方法,以及在分析期间应该应用Bandera工具集中包含的哪些工具。Java源代码和字节码已经生成,但还需要创建会话文件。我们已经在VisualBasic Script中实现了一个脚本,它用Java源代码和字节码的位置以及包含main方法的类来更新模板Bandera会话文件。会话文件包含调用Bogor进行死锁检测和断言的命令违规检查,以及将程序的BIR模型输出到文件的工具。当Bandera预处理器完成时,结果是一个功能齐全的Bandera会话文件,以及程序的可验证BIR模型3.3.2断言后处理器。断言后处理器扫描Java源文件,以查找断言前处理器创建的用户定义断言的任何指示(如第3.1.1节所述)。如果检测到断言的使用,则已定位的内容将被有效的Java断言语句替换。这一步是通过一个简单的Visual Basic脚本实现的。3.3.3源代码编辑器。由于断言后处理器可能会导致Java源代码发生变化,因此需要重新编译源代码,以确保我们的Java类文件(字节码)正确地反映更新的源代码。Java SDK提供的Java编译器用于此编译。3.4关于BanderaMSILCAD的最后一步是从已生成的Java源代码中提取BIR模型。生成的会话文件被输入到Bandera,BIR模型被提取,BogorTool被调用来分析BIR模型的死锁和断言违规。分析结果显示为Java字节码班德拉Java编译器断言后处理器Bandera预处理器14J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3错误/toolResult>![CDATA[ [Time:3516 ms,Depth:282] Error found:Invalid end state搜索前总内存:93,079,928 bytes(88.77 Mb)搜索后总内存:93,257,000bytes(88.94 Mb)总搜索时间:3563 ms(0:0:3)状态计数:281匹配状态计数:9最大深度:282完成!]]/toolResult>见图8。 Bandera结果:僵局C#编程Javapublic class Uncle{private bool [] buf;private int inn;private int outt;private int count;private int size;private int i;public int findDuplicate(int nums){这个尺寸=尺寸;buf = new bool [size];for(i=0; i size; i++)int count =0; int count= 0;}public booleancanCatchTheft(){while(count==size)Monitor.Wait(buf); buf[inn] = b;计数++;inner =(inner + 1)%size; Monitor.Pulse(buf);}}public void onResume(){while(count==0)Monitor.Wait(buf); buf[outt] = false;count--;outt=(outt + 1)% size; Monitor.Pulse(buf);}}}public class Uncle{public boolean buf [];private int count;private int size;private int i;public int findDuplicate(int j){return j;buf = new boolean[j]; for(i = 0; i j; i++)int count = 0; intcount = 0;}public boolean alert(boolean alert){while(count == size)try{buf.wait();} catch(InterruptedExceptioninterruptedexception){ }buf[inn] = flag;计数++;int n =(n + 1)% size;buf.notify();}}public void onDestinyNode(){while(count == 0)try{buf.wait();} catch(InterruptedExceptioninterruptedexception){ }buf[outt] = false;count--;int n =(int n + 1);}}}见图9。有界Buffener变换控制台上的纯文本4变换和实验为了评估我们的框架,我们使用了三个例子:用餐哲学家,Bounded Bu和彼得森对于J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)315每一个例子,我们的评估-16J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3这个过程涉及到用C#和J#语言编写算法,并(手工)验证我们到Java的转换是否正确执行。通过检查目标的执行和模型检查行为是否与源的原始语义匹配,我们证明了语义在所有转换中都得到了很好的保留。最后,我们应用模型检查进行死锁检测,并插入断言语句来测试断言冲突。4.1哲学家进餐我们使用五个哲学家和监视器实现了两个版本的用餐哲学家问题第一个版本是无死锁的,而第二个不是。我们用Bandera分析了这两个版本以测试死锁,两个分析都产生了预期的结果。图8显示了分析结果的BogorTool它表示在允许死锁的示例中发现了死锁。4.2有界缓冲器Bounded Buffer算法是一个有趣的转换示例,因为它包含对象锁定,各种监视方法(Wait,Pulse)和异常处理。图9展示了BufferImpl类从C#到Java的完整源代码转换,它取自BoundedBuffer示例。4.3PetersonPeterson我们使用MSILCAD和Bandera对于大量的进程,我们的翻译是成功的,但茂物耗尽了内存。4.4选定的转换表3展示了对于Dining Philosophers和Bounded Buchener两个示例,每个工件所产生的代码行数。正如预期的那样,对于两个示例,源语言(C#和Java)的代码是相似的。Java包含更多的异常,大部分是因为Java字节码工件(MSIL、JASMIN)的重复数也相当。MSIL有更高的计数,因为它包含一个所有转换都应用于Intel Pentium 4,1.6Ghz CPU,512MB RAM,转换时间可以忽略不计。J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)317表3翻译工件哲学家进餐有界缓冲器C#语言6788MSIL276364JBC232298Java811225相关工作当前的软件模型检查器大致分为两类。第一种是基于一个翻译框架,它将源语言中的程序转换为用现有模型检查器的输入语言表示的等效有限状态机。Bandera(Java)[3]和Feaver(C)[7]都是基于这个概念。在第二类软件模型检查器中,标准运行时环境被实现检查的定制环境所取代。这一类的例子包括Java Pathworld(用于Java)[18],VeriSoft(用于C/C++)[5]和Zing(用于MSIL)[1]。就像Zing一样,我们的方法针对MSIL。然而,它与Zing的不同之处在于它是基于警告的。此外,我们利用Bandera工具集的现有优化和在撰写本文时,正在为Java字节码开发一种新的模型检查方法。Bogor和Bandera的作者介绍了BogorVM的早期原型 [14],一个直接针对Java字节码而不是源代码进行模型检查的模型BogorVM还处于开发的早期阶段,有其局限性,因此我们使用Bandera来实现我们的目的。在[ 16 ]中对微软的公共语言JVM(Common Language JVM)和Java虚拟机(Java Virtual Machine)进行了比较这项工作包括从一个子集的Java到JVM的我们的工作在这方面是类似的,但超越了虚拟机的比较,通过模型检查对软件进行正式验证,转换框架直接作用于Microsoft源代码,并产生相应的Java源代码。此外,我们的转换还支持断言的使用,以及Bandera转换后对这些断言的自动验证。最后,我们能够利用源代码转换技术,以方便和高级的方式实现易于扩展的翻译6结论和今后的工作我们已经提出了一种方法,通过利用Microsoft中间语言(MSIL)的“多对多”特性来对.NET语言家族进行模型检查。该方法使用源代码转换将MSIL转换为Java18J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)3字节码然后使用Bandera工具集优化和分析结果字节码。我们已经实现了一个原型的方法,并评估了它与几个小的例子有希望的结果TXL被证明是一个方便的工具来实现翻译。虽然我们的原型目前还没有处理一些语言功能,但我们没有看到为什么它不能扩展到不仅支持MSIL的整个安全子集,而且支持其他.NET语言(如VisualBasic)的原因。该项目近期的工作包括扩大翻译范围。更准确地说,翻译将得到改进,以处理更大的J#和C#子集以及其他.NET语言,如Visual Basic和C++。此外,为了获得模型检查的全部好处,应该添加对时态为了使分析更加用户友好,Bandera产生的任何反例都应该映射回原始源。换句话说,应该应用标准技术来使我们的TXL翻译“完全可逆”。最后,将MSIL直接翻译成BIR将成为另一个更长期的研究课题。引用[1] 安德鲁斯,T.,Qadeer,S.,Rajamani,S.K.,J. 和Xie,Y.Zing:并发软件的模型分析,技术报告MSR-TR-2004-10,MSR(2004)。[2] Cimatti,A.,Clarke,E.,Giunchiglia,F.和Roveri,M. NUSMV:一个新的符号模型检查器,国际软件工具技术转让杂志2(4)(2000),410[3] 科贝特,J.,德怀尔,M.,Hatterygal,J.,Pasareanu,C.,罗比,劳巴赫,S.,和Zheng ,H.Bandera:Extracting Java Source Code,第22届软件工程国际会议(2000)。[4] 科迪,J.R.,迪恩TR Malton,A.J.,和Schneider,K.A. 使用TXL转换系统进行软件工程中的源代码转换,信息与软件技术杂志44(13)(2002),827[5] Godefroid,P.,Software Model Checking:The VeriSoft Approach,Formal Methods in SystemDesign。26(2)(2005),77-101.[6] Holzmann,G.J.[7] Holzmann,G.,史密斯,M.H.软件模型检查-从源代码中提取验证模型,协议工程和分布式系统的形式化方法(1999)。[8] Kouznetsov,P. Jad -快速Java反编译器。网址:http://www.kpdus.com/jad.html。[9] Lidin,S. “Inside Microsoft .NET IL Assembler”, Microsoft Press,[10] Lindholm,T.和Yellin,F. “The Java Virtual Machine Specification”, Addison Wesley,[11] 迈耶,J.,和Daud,D. 04 The Famous Famous(2004) 网址:http://jasmin.sourceforge.net/。[12] 彼得森,G.L. 关于互斥问题的神话,信息处理信件。12(1981),115-116.[13] Platt,D. S. “Introducing Microsoft .Net”, Microsoft Press,J. McGeachie,J.Dingel/Electronic Notes in Theoretical Computer Science 190(2007)319[14] 罗比BogorVM:Customizing Bogor for model checking Java programs homepage(2006).网址:http://bogor.projects.cis.ksu.edu网站。[15] Robby,Dwyer,M. B.和Hatterygal,J.Bogor:一个可扩展的和高度模块化的模型检查框架,欧洲软件工程会议和ACM SIGSOFT软件工程基础研讨会(2003年)。[16] Shiel,S.贝利,我。A Translation-Facilitated Comparison between the Common Language XML andthe Java Virtual Machine,Proceedings of the First Workshop on Bytecode Semantics,Verification,Analysis and Transformation(2005).[17] Sutter,H.免费的午餐结束了:软件并发性的根本转变。Dobb的日记30(3)(2005)。[18] Visser,W.,Havelund,K.,布拉特,G.,公园,S.,和Lerda,F. 模型检查程序,自动化软件工程杂志。10(2)(2003年)。
下载后可阅读完整内容,剩余1页未读,立即下载
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)