理论计算机科学电子笔记141（2005）153-169www.elsevier.com/locate/entcs在证明助理中正式确定AADL1David Chemouil2 Mamoun Filali3 Martin Strecker4IRITUniversit′ePaulSabatier118 route de NarbonneF-31062 Toulouse摘要本文介绍了架构分析和设计语言的形式化的第一步，主要集中在其数据模型的表示。为此，我们对比了两种方法：一种是基于集合的（使用B建模框架），另一种是高阶逻辑（使用Isabelle证明助手）。我们说明了AADL元模型的简化部分的转换有关的流。保留字：AADL，程序转换，定理证明1介绍本文讨论了AADL（架构分析和设计语言）[10]的正式元模型的设计决策，AADL是一种已于2004年10月成为SAE5的AADL是以前的架构描述语言的综合，如MetaH [17]，Acme [11]和Cotre [5]。AADL作为一种体系结构描述语言，1 电子邮件地址：bodeveix@irit.fr2 电子邮件：david. cnes.fr3 电子邮件：filali@irit.fr4 电子邮件地址：strecker@irit.fr5 汽车工程师1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.008154J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153以及静态方面，如划分成包和动态方面有关的活动实体，它们之间的通信和定时方面。事实上，它反映了日益增长的工业需求，即对复杂的软件/硬件工件进行建模和推理，如航空电子和汽车领域。事实上，这篇文章的作者是联邦项目的合作伙伴它由空客等公司组成，旨在创建一个工作台，其主要建模语言是AADL。由于其应用领域的复杂性，AADL本身的定义是大量的，不容易获得。除了AADL标准，Ecore中还有一个形式化的描述，Ecore是XML的一个变体，将在第2节中进行总结。就其本质而言，后者只能捕获语法方面和有限的类型形式，但不能捕获模型的某些一致性条件（在TOPCASED项目的上下文中，我们对描述AADL模型转换及其原因感兴趣，目的是证明，例如，• 它们保留了模型的语义，或者至少某些语义方面，例如时间行为。这是必要的，尤其是当转换模型时，以便它可以被其他验证工具（如模型检查器）处理• 他们保留或建立特定的财产。这种格式良好性检查适用于可能更改模型语义的重构步骤。定义编程语言的形式语义并在证明助手中验证语言转换或编译器的正确性是一种行之有效的做法。出于几个原因，AADL并不完全适合这个计划：• Ecore风格的表示给了它一个面向对象的工具。然而，大多数证明助手都是基于集合论或高阶逻辑的形式，包括一种函数语言。尽管面向对象概念的编码是可能的（“深嵌入”），但使用底层证明助手（“浅嵌入”）所提供的语言概念来我们将在第3节讨论几种替代方案。• AADL的庞大规模（200个类，通常具有大量的属性）使得手动处理变得困难。此外，由于AADL标准的新近性，Meta模型的频繁改变可能是不可避免的。预期因此，将Ecore表示转换为选择的证明助手的定义的至少部分自动化是合理的。J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153155我们将在整个文本中指出如何实现这一点目前，我们只能对AADL语言的形式化给出一个非常初步的描述。尽管还不完整，第4节中的一个小例子显示了我们的方向。本文在第5节结束，讨论了相关的工作和可能的扩展。2Ecore语言定义Ecore是EMF的元模型，EMF是Eclipse建模框架。在[6]中，EMF被描述为因此，EMF定义了包、类、对象和属性等概念Ecore本身是以XML模式的形式呈现的[8];因此，Ecore的定义，如AADL的定义，都是XML文档。这些文件可以自动处理.为了直观起见，考虑以下类别的定义，为了这个演示的目的稍微简化：它定义了一个类AObject（AADL类层次结构的最顶层），它的一个直接子类NamedElement和一个Connection类。类AObject可以包含任意数量的注释属性（如负upperBound所示），NamedElement有一个name属性，除了 从 AObject 继 承 的 注 释 属 性 。 具 有 超 类 型 ModeMember 和ReferenceElement的Connection具有三个（非继承的）属性，其中两个是对类ModeMember Context的元素的引用（连接的源和目的地）。Ecore本身没有正式的语义。当然，定义一个语义-156J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153tics for XML [25]并没有给借助XML定义的语言（如Ecore）赋予意义大多数情况下，Ecore与UML或Java相对应[9，6]，但也不是以系统的方式。总而言之，我们只能根据对基本概念的非正式理解，自己给Ecore的我们将在第3节中探讨不同目标形式主义的这种翻译，不仅限于AADL的定义，而且可以应用于Ecore中定义的任何语言然而，AADL施加了一些额外的约束，这些约束不能在Ecore中表达，但在附带的标准中得到了精确的描述[14]。到目前为止，我们还没有涵盖Ecore的全部内容，但要特别注意以下几个要素：• 类和属性，由eClassifiers和eStructural- Features元素表示• 类层次结构，如Ecore类的eSuperTypes属性所表示的，以及抽象性（属性抽象）。• Ecore属性的类型（eType）以及多重性（下限和upperBound）。其他元素（eAnnotations）目前尚未处理。不遵守封装结构（即，我们假设一个单独的包），因为Ecore允许跨包边界的元素之间的相互依赖，这对于第3节中使用的系统是不可接受的。3模型定义：备选方案在本节中，我们考虑Ecore语言中描述的编码模型的两种替代方案第一个是基于集合论，第二个是基于高阶逻辑。3.1基于集合的编码在本节中，我们将说明如何在集合论中编码一个ecore描述。我们使用B [1]语法。转换到其他基于集合的框架，如TLA [16]或Isabelle-ZF [23]应该是类似的。在本节中，我们将概述数据建模的原则在第4节中，我们提出了一个转换，这是一个依赖于这样一种表达的例子。我 们 考 虑 一 个 简 单 的 类 层 次 结 构 ， 其 中 AObject 是 根 ， 并 且 类AqentImpl和AqentType是从类AqentClassifier派生的。J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153157类层次结构。基于集合的编码的基本思想是将面向对象程序设计的is-a关系表示为集合论的子集关系，并将C类型的整个对象集合（Csub集合）划分为将是C的实例（C集）和对象，其类型是C.然后，这样的分区将是实际创建的实例的容器：与类C相关联的分区将包含类C的实例。因此，不同类的实例集将是不相交的。最后，当类C是抽象类时，容器C被置为空，即，我们有一个额外的性质：C = 0。在B中，我们将其编码如下6：集AObject /*AADL对象的宇宙*/常数/*容器*/属性分类器、属性实施、属性类型定义分类器sub ==（数据分类器∪隐私政策System. out. println（）;性能分类器AObject/*容器不相交*/∧分类器Submitted Classifiersub-（Submitted Typesub Submitted Implsub）∧联系我们Subclassifiersub-（SubclassifierSubclassifierTypesub）联系我们PencientClassifiersub-（PencientClassifier PencientImplsub）属性和属性。由于我们计划研究模型转换，因此实例必须是动态的，并且由作为AObject子集的变量实例编码。此外，正如我们将在第4节中看到的，类C的一个新实例作为C -实例的一个元素获得。对于前面的例子，我们有：变量/*实际创建的实例*/ instances6在B中，FIN（A）是A的有限子集的集合;定义引入（参数化的）宏。158J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）1532不变实例AObject备注。在B的上下文中，为了定理证明的目的，我们还可以陈述以下断言，即，一个谓词，可以从前面的属性和不变量导出：断言安装 联系方式=因为有n×（n−1）个派生谓词，所以应该只为具有少量派生的类自动生成这样的断言美德.先知-愿类的属性表示为函数。为了支持继承，这些函数的域是类及其派生的实例的集合。然后，我们有：变量class属性，.不变classattribute∈ Classsub实例→typeattribute我...读取实例o的属性i包括计算classattribute（o）。而o的更新和属性很容易通过B的重载表示法来表示：classattribute（o）：=新属性值3.2基于高阶逻辑的在下文中，我们将介绍在高阶逻辑中对AADL元模型进行编码的第一步。更具体地说，我们展示了如何在Isabelle/HOL[ 20 ]中表示Ecore的关键元素，如第2节所介绍的，Isabelle/HOL是通用证明助手Isabelle的高阶逻辑扩展。我们将主要限于Isabelle/HOL的核心（具有ML风格多态性和归纳数据库的简单类型这有双重优势：首先，我们的开发可以很容易地转移到其他具有更有表现力的类型系统的证明助手，如Coq或PVS;其次，我们仍然停留在传统编程语言的类型系统领域，如ML，这样我们就可以在标准平台上获得可执行的验证代码[4]J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153159让我们回顾一下主要的选择：深度嵌入并不试图将语言的元素直接表示为目标语言的表达式（在本例中：Isabelle/HOL），而是对它们进行编码。例如，类可以由类名、超类的名称和它们的属性类型的列表来表示在[22]中描述的Java语义中遵循了这种方法我们会得到一个定义，attrib_decl= attrib_name* attrib_typeclass= cname * cname * attrib_decllist在我们的设置中，乍一看，这看起来很有吸引力，因为它允许非常统一的处理，并且从Ecore到证明助手的语言的翻译几乎是立即的。然而，也有严重的缺点：几乎没有提供来自证明辅助的底层类型系统的保护例如，一个类的实例是一个属性值的列表：inst=（attrib_name* value）列表类和实例应该具有相同数量的属性，属性值具有正确的属性类型，这一事实必须表示为谓词，并且不能由类型系统确保此外，请注意，我们正在处理的类结构不是开放式的，不像传统的面向对 象 程 序 那 样 。 相 反 ， 类 结 构 是 固 定 的 。例 如 ， FlowSpec 可 以 是FlowSourceSpec， 一FlowSinkSpec或FlowPathSpec。这一事实将再次被编码明确地说，而我们更愿意诉诸归纳原则。所有这一切使我们考虑一个浅嵌入，其中AADL类被编码为HOL的类型，而类的实例对应于相应类型的术语。让我们再一次阐明我们的愿望，然后看看我们能在多大程度上满足它们：“Subclassing”应该对应于“subtyping”。不幸的是，在ML样式的类型系统中，我们没有“子类型”的自然概念最好的情况是，我们可以利用多态性来编码子类型。事实上，这是Isabelle的可扩展记录的基本思想例如，一个类A，a：nat和它的子类B以及字段a：nat，b：bool将产生类型定义数据类型’a’b160J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153’a A’b因此，项c A 3（c B True（））的类型为单元B。函数获取a，选择a属性并定义为常数get_a：：get_a（c_A a x）= a将适用于类型A和类型B的元素。这种方法很优雅，但是：• 类型系统不允许表达这样一个事实，即A只有特定的子类，比如B和C。• 我们不能形成一个类及其子类的所有元素的集合（如列表或集合），因为这些元素将具有不同的类型，即使是相同类型模式的实例。然而，为了表达一些格式良好的约束（例如近年来，在类型化lambda演算中对面向对象语言进行编码的研究激增[2，13，7]。它们中的大多数都是基于System F的扩展，因此离开了简单的ML样式多态性的框架，因此对我们没有直接的用处第二种方法是分解类层次结构。对于上面的A类和B类，我们将得到类型A =natB =nat * bool这会让我们失去A和B之间的联系特别是，我们不能以统一的方式定义像geta这样的访问器函数，而必须诉诸重载，这是Isabelle的一个特殊功能，在其他证明助理中提供：常数get_a：：get_a_A：get_a == idget_a_B：get_a ==fst这种缺乏统一性的情况使我们避免采用这种解决办法。这使我们得出最终采用的解决方案。为每个类J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153161C，我们定义了两种类型：• 一个C型，它是C亚型的总和。对于非抽象类，我们为C类的实例添加一个进一步的组件（类型为Unit），而不是它的子类。对于没有子类型的类，我们不构造sC。• 一个类型tC，它是C的属性类型和C（如果存在）。例如，对于在3.1节中提到的Classifier类，我们得到类型定义datatype s_questionClassifier=cs_certaintType t_certaintType| cs_concilientImplt_concilientImpldatatype t_questionClassifier =ct_questionClassifier oid s_questionClassifier其中，s PencentClassifier对该类具有子类PencentType和PencentImpl这一事实进行编码。 类不是抽象的，否则我们会有另一个构造函数cs Unit。我们稍后将回到oid组件。当从类层次结构的叶子到根进行这种构造时，我们最终得到一个类型，对应于所有对象的类，在我们的例子中是AObject因此，不幸的是，我们不得不放弃类和类型之间的一一对应：因为目标不可调和的是，我们选择放弃前者，支持后者。然而，我们可以通过谓词来编码类成员关系，比如是组件分类器。这些用于表示模型上的某些一致性条件，如下所述。一般来说，AADL模型将具有图结构，因此组件将通过引用（Ecore中的EReference类型）相关联。 为了对对象标识进行建模，我们引入了一种对象标识符类型oid，我们将其实现为自然数以简化某些操作，例如创建一个“新”oid：常量定义new_oid：： oidlist => oidnew_oid os ==（foldl max 0 os）+1162J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153我们用一个oid属性t_AObject =ct_AObject oid s_AObject现在可以将AADL模型定义为对象的集合类型AADL_Model= t_AObject列表新实例的创建，例如对于类Component（参见示例第4节），是相对于AADL模型M来完成的，具有诸如new Component M nm的表达式。对模型的最低要求是格式良好，包括：• 对象标识符• 属性的类型正确性，特别是引用。请注意，这个属性通常不能被类型系统静态地强制执行，因此对模型的修改将生成证明义务。例如，我们说一个组件是良好类型的，如果它的实现引用im是一个martentImpl，它的所有端口po都是良好类型的，它的子组件和martow组件也是如此：常数wt_Component：： [AADL_Model，t_Component]=> bool primrecwt_ComponentM（ct_Component im po pafl）=（（option_lift（reftype Mis_Optional Impl）im）/\（list_all is_Portpo）/\（option_lift（reftypeMis_Flow Impl）pa）/\（list_allis_Flowfl））这结束了我们的描述我们的AADL形式化。我们正在完善该模型，以包括AADL标准中表达的进一步一致性条件。4示例：流量在本节中，我们将概述如何在我们的框架中考虑转换。 我们首先给出AADL元模型的一部分，然后定义一个简单的转换，增加了一个过滤器到一个流。这个例子是用B语言开发的。J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）1531634.1AADL元模型在这个例子中，我们考虑AADL元模型的一个简化部分，它描述了一个流的概念。在组件的规范中，可以将端口流声明为输入端口和输出端口之间的连接。在该实现中，并行流可以遍历子组件。存在三种类型的湍流：湍流路径、湍流源和湍流汇。我们在这里考虑可以使用以下正则表达式定义的流路径：flow_path：：= port（connection flow_path）* connection port|端口port迭代（连接/流路径）对表示子分量遍历。 它们在元模型中使用引用一个连接和一个流路径的流元素的有序序列来定义。端口由Connection类的实例表示引用为srcDst（图1）。Fig. 1. 简化AADL模型使用前面解释的原理将元模型转换为B常量、抽象变量和4.2转换示例让我们考虑在一个组件的给定路径上引入一个滤波器的变换。图2说明了这种转变。164J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153ImpFPImp滤波器FPadd_filter（imp，fp，filter）图二. 添加过滤器应用这种转换会导致创建多个对象，例如过滤器组件、其输入和输出端口以及它们之间的流路径然后将过滤器作为实现的子组件添加，并插入到作为参数给出的流路径转换必须分配新对象。它们是在其类的未分配元素集中选择的同一个类的对象被显式声明为不同的。例如，下面的代码片段声明了FlowElement和Connection的自由实例中的两个新对象。任何地方fe： FlowElement-实例cnx：连接-实例然后...端然后将声明的对象添加到实例集instances：=instances{ fe，cnx}最后，必须建立对象之间的连接。为此，更新（功能或非功能）关系。例如，过滤器子组件的过滤器路径和将组件的输入端口链接到过滤器的输入端口的连接初始化过滤器元素。FlowElementscFlowPath（fe）：= f_fp|| 流元素连接（fe）：=cnx上面给出了转换的完整代码这些操作的前提条件断言给定的滤波器正好有一个输入端口和一个输出端口，它们之间有一条流水路径这个流路径将被插入到给定组件实现的流路径fpAddfilter（imp，fp，filter）=预imp：（imp实例）impJ. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153165fp：流（imp）流fp： dom（FlowPathconnection）流过滤器：（组件流实例）流卡（流端口（过滤器））=2流 Portdir[流端口（过滤器）]={ In，Out}流流（过滤器）流FlowPath流卡（流端口（过滤器））=1然后任何p_in、p_out、fe、cnx、f_fp、sc，其中p_in：parent（filter）blog_out：blog（filter）Portdir（p_in）=In端口目录（p_out）= Out实例：FlowElement-实例连接-实例footsf_fp：过滤器（filter）子组件- 实例然后instances：=instances{ fe，cnx，sc}/*初始化流元素*/||FlowElementscFlowPath（fe）：= f_fp|| 流元素连接（fe）：=cnx||FlowElementsc（fe）：= sc||Connectiondst（cnx）：= p_in/*子组件插入*/||Subjectienttype（sc）：= filter|| 次级母体（sc）：=杂质||安装子组件：=安装子组件{imp›→sc}|| IF FlowPathflowElement(fp)/=[] THENLET fe1,cnx1 BEFE1=first（FlowPathflowElement（fp））cnx1 =流元素连接（fe1）INConnectionsrc：= Connectionsrc +{ cnx1›→ p_out，cnx›→Connectionsrc（FlowPathsrcDst（fp））}端其他Connectionsrc（cnx）：= Connectionsrc（FlowPathsrcDst（fp））端/*插入过滤器*/||FlowPathflowElement（fp）：= fe-> FlowPathflowElement（fp）端166J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153结束结束这种变换的具体化允许验证静态属性，例如保留由不变量指定的模型的良构性属性这里考虑的属性是由元模型直接表达 它们可以很容易地在B级进行扩展：必须很好地构建流路径，以便连接的末端和子组件流路径的末端相匹配。此外，组件的实现和规范必须是兼容的，这意味着它们具有相同的端口，并且流路径的源和目的地是相同的。这些不变量确保转换保留了模型的基于XML为了更进一步，转换的抽象规范应该表示指定的流程是通过遍历过滤器实现5结论我们已经提出了将Ecore语言翻译成不同形式主义（基于集合的高阶逻辑）的方法特别是，我们感兴趣的AADL Meta模型，这使我们能够指定和证明正确的转换AADL模型的表示。似乎基于集合的方法非常适合我们的关注。然而，由于高阶逻辑证明助手（Coq，HOL，Isabelle，PVS）通常可用的框架的力量，务实的方法将是在高阶逻辑中嵌入集合论我们进一步研究的一个主要问题是这种嵌入方法的可扩展性。我们没有进一步探讨的一个途径是：将AADL类结构视为面向对象程序的类结构，将转换视为这些类的适当方法为了证明变换的正确性，证明这些方法对于特定的规范是正确的。证明可以使用面向Java的工具[15，18，19，12]或面向OO的规范机制，如Object-Z或变体[24]。即使我们没有具体的证据，我们怀疑OO程序的验证比我们选择的方法更我们相信通常在逻辑框架中可用的抽象机制更适合。一个众所周知的事实：我们感谢尼科拉斯·拉尔为我们提供的帮助。J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153167一B编码本节给出了一个B代码的示例。只有转换的文本，即，B操作Addfilter（第4节）已编写。机器子句：集合、具体常数、定义、属性、抽象变量、不变量和初始化。TIALISATION是从Ecore描述的AADL模型的简化片段中自动获得的（翻译器是CDuce [3]和Ocaml的组合机器人玩具集String;AObject;Direction={In，Out}混凝土常数FlowS ource，FlowSi nk，F lowElement，NamedElement，F low，Connection，Componnt， 子组件、部件、组件实施、流路径定义FlowSourcesub（FlowSource）;FlowSinksub（FlowSink）;FlowElementsub（FlowElement）;NamedElementsub（ 一）NamedElement流子流Portsub 联系我们 隐私政策 browser（sub）;...性能FlowSource流源对象流汇对象流元素对象命名元素对象流流对象对象...抽象变量首先，F l ow S ur c e p o r t、F l ow S i nk p o r t、F l ow Eleme n tcon n ectio n、F l ow Eleme ntscF l ow P a t h、N a medEleme n t name、C o nn e c t i on s r c、C o nn e c t i on d s t、C o m pone n tip l、C o n e n t p or t，Sub C om p o n e n t p a r e n t p a r e n t，Compo n e n t a r w，P or t d i r，C om p o n e n t Imp l un n m e d，C om p o n t Impls p e c，C om p o n t ImplSu b c p on t，C om p o n t Implo w，C om p o n t Implconnectio n，F l o w P a t h o w E l e m e n t，流媒体连接、流媒体源代码、子组件类型不变实例 联系我们FlowSourceport∈（ FlowSourcesub实例）−→（Portsub实例）<$FlowSinkport∈（ FlowSinksub实例）−→（Portsub实例）<$FlowElement连接∈（FlowElementsub 实例） −→（连接sub 实例）...初始化instances：=实例 FlowSourceport ：=流汇端口 ：=FlowElementconnection：=流元素 FlowElementscFlowPath：=流命名元素名称：=流连接源：=流连接dst：=流连接源：=流连接端口：=流连接父：=流组件流：=流端口目录：=流组件...操作加上filter（imp，f p，filter）/*seesectionIV。* */端168J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153引用[1] J.R.阿布里尔B-Book是一种对意义的编程。剑桥大学出版社，1996年。[2] 我是ABADI，LUCACDL I，RA M A B A D I，R A M A C一个不包含对象接口和对象类型的实例 。在ACM Symposium on Principles of Programming Languages （ POPL ） ，St.Petersburg Beach，Florida，第396-409页[3] V. Benzaken，G. Castagna和A. 弗里施 CDuce是一种以XML为中心的通用语言。ACMInternational Conference on Functional Programming，2003。http://www.cduce.org/papers.html网站。[4] Stefan Berghoun和Tobias Nipkow。执行高阶逻辑。在Proc. TYPES工作组2000年年会上，LNCS，2000年。[5] B. Berthomieu，P.O. Ribet，F.Vernadat，J.L. Bernartt，J.-M. Farines，J.P. Bodeveix，M.菲拉利湾Padiou，P. Michel，P. Farail，P. Gau fillet，P. Dissaux，and J.- L.兰伯特 航空电子实时系统的验证：Cotre方法。在第八届国际工业关键系统研讨会上，ROROS，第201托马斯艺术，Wan Fokkink，2003年6月5-7日。[6] Frank Budinsky，David Steinberg，Ed Merks，Ray Ellersick，and Timothy Grose. Eclipse建模框架。Addison-Wesley，2003年。[7] 阿德里亚娜湾 康帕尼奥尼具有交集类型的。博士论文，荷兰奈梅亨大学，1995年1月。ISBN 90-9007860-6。[8] 万维网联盟。 可扩展标记语言（XML）。http://www.w3.org/XML/网站。[9] EMF：Eclipse建模框架。http://download.eclipse.org/tools/emf/scripts/home.php网站。[10] Peter H. Feiler，Bruce Lewis，and Steve Vestal. SAE架构分析设计语言（AADL）标准：基于模型的架构驱动嵌入式系统工程的基础。《2003年区域技术评估讲习班》，第1-10页[11] 放大图片作者：Robert T.门罗和大卫·怀尔Acme：一种体系结构描述交换语言。在CASCON'97的会议记录[12] M. Huisman和B.雅各布斯高阶逻辑中的继承：建模和推理。在Proc. Theorem Proving inHigher-Order Logics，1869卷Lecture Notes in Computer Science，第301 - 319页。SpringerVerlag，2000年。[13] 马丁·霍夫曼和本杰明·皮尔斯阳性亚型。信息与计算，126（1）：186[14] SAE国际。 架构分析设计语言（AADL），2004年8月。[15] BartJacob s，ClaudeMar ch′e，and NicoleRau ch. Formalverificationofacommercialsmartcardapplet with multiple tools.2004年[16] 莱斯利·兰波特TLA+语言和工具，硬件和软件工程师。Addison-Wesley，2002年。[17] MetaH。http://www.htc.honeywell.com/metah/网站。 一九九七年。[18] Clau d eMarch′e，Chr istinePa u lin-M ohr i n g，andX av ierUrb ain.K致力于对JML注释的JAVA/JAVACARD程序进行认证。Journal of Logic and Algebraic Programming，58（1http://krakatoa.lri.fr网站。[19] 彼得·穆勒。 ModularSpecicionanddVericionofObjectedPrograms，volume2262 ofLecture Notesin Computer Science.Springer Verlag，2002年。J. - P. Bodeveix等人理论计算机科学电子笔记141（2005）153169[20] 托拜厄斯·尼普科劳伦斯·保尔森马库斯·温泽尔。Isabelle/HOL.高阶逻辑的证明助手。LNCS 2283.Springer Verlag，2002年。[21] 沃尔夫冈·纳拉舍夫斯基和马库斯·温泽尔。高阶逻辑中基于记录子类型的面向对象验证。在Theorem Proving in Higher Order Logics，TPHOLsSpringer，1998年。[22] 大卫·冯·欧海姆布。 在Isabelle/HOL中分析Java：形式化，类型安全和Hoare日志。PhDthesis，Techn ischeUn iversititétMunénchen，2001. http://www4.in.tum.de/http：//www.example.com[23] 劳伦斯·保尔森。伊莎贝尔的逻辑：FOL和ZF。技术报告，剑桥大学，计算机实验室，2004年。可从http://www.cl.cam.ac.uk/Research/HVG/Isabelle/获得。[24] 托马斯·桑滕。Isabelle/HOL中基于结构化模型的规范理论。在Proc. Theorem Proving inHigher-Order Logics，计算机科学讲义第1275卷，第243-258页Springer Verlag，1997年。[25] 杰罗姆 西缅 菲利普·瓦德勒的 XML的本质在Proc.POPLhttp://homepages.inf.ed.ac.uk/wadler/topics/xml.html网站。
我的内容管理
展开
