『OCL规范对JAVA CARD程序规范和验证的背景评估』

理论计算机科学电子笔记102（2004）3-19www.elsevier.com/locate/entcsOCL中的丹尼尔·拉尔森1沃伊切赫·莫斯托夫斯基2瑞士查尔姆斯理工大学计算机科学系摘要我们将讨论JAVA CARD API的OCL规范的开发本规范的主要目的是支持和帮助验证KeY系统中的JAVA CARD程序KeY系统的主要目标是集成面向对象设计和形式化方法。用JML（JAVA建模语言）编写的现有规范已被用作OCL规范开发的起点在本文中，我们报告了我们在编写规范时遇到的问题及其解决方案，我们介绍了规范中最有趣的部分，我们报告了成功的验证尝试，最后我们评估了OCL，并将其与JML在JAVA CARD程序规范和验证的背景关键词：OCL，JML，JAVACARD，形式化规范，形式化验证，面向对象设计1介绍本文报告了JAVA CARD API的OCL规范的开发[19]。JAVA CARD [9]是JAVA编程语言的一个子集，用于对智能卡进行编程。JAVA CARD API（应用程序编程接口）是一组用于JAVA CARD程序的库类。JAVA CARD API是标准JAVAAPI的一个小得多的版本，专门为智能卡编程而设计。当API类的实现不可用时，OCL规范对于执行此类程序的正式验证是必要的即使API实现是1电子邮件地址：it3lada@ituniv.se2电子邮件地址：woj@cs.chalmers.se1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.09.0014D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）可用，具有OCL规范有助于避免每次在JAVA CARD程序中使用API方法时提供API实现的重复工作编写规范的第二个目的是以正式的方式记录JAVACARDAPI的行为。我们讨论了在OCL中编写规范时遇到的问题及其解决方案。我们介绍了规范中最有趣的部分，并报告了JAVA CARD APIw.r.t.参考实现的成功验证尝试。我们的规格。最后，我们评估了OCL，并将其与JML进行了比较。本文总结了[11]的结果。在接下来的部分中，我们将详细介绍这项工作的背景和动机。在第3节中，我们详细报告了规范的发展，在第4节中，我们介绍了规范中一些有趣的部分，在第5节中，我们在所介绍的工作的背景下评估了OCL，最后，我们在第6节中总结。2背景2.1重点项目本文所介绍的工作已作为KeY项目的一部分进行[1，2，10]。KeY项目的主要目标是增强商业CASE（计算机辅助软件工程）工具，使其具有正式规范和演绎验证的功能，从而将正式方法集成到现实世界的软件开发过程中。因此，KeY系统软件验证部分的设计原则为：(i) 规范语言应该能被那些没有经过多年正规方法培训的人使用。对象约束语言（OCL）[14]，它被合并到统一建模语言（UML）的当前版本中，是我们选择的特定语言(ii) 被验证的程序应该用“真正的”面向对象的编程语言编写。我们决定 使 用JAVA CARD 。 这 一 选 择 是出 于 以 下 原 因 。 首 先， 许 多JAVACARD应用程序都要经过正式验证，因为它们通常是安全关键的（例如身份验证），并且在发现故障时难以更新。同时，JAVACARD语言比完整的JAVA更容易处理（例如，没有并发性和GUI-参见第2.2节）。此外，JAVA CARD程序比正常的JAVA程序小，因此更容易验证。KeY系统的架构如图1所示。它建立在一个商业CASE工具（BorlandTogether Control Center [7]）之上，D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）5CASE工具延伸用于正式规范UMLOCLJava验证中间件动态逻辑演绎组件自动化互动Fig. 1. 关键系统它具有通过以下方式正式规范和验证JAVA程序的设施：• 它支持创建和操作OCL约束，例如，KeY系统可以通过实例化OCL模板（常用的OCL规范模式）自动创建部分OCL规范，或者使用基于语法的编辑器创建OCL表达式。• 演绎组件用于实际构造从UML模型、OCL约束和JAVA实现生成的JAVA动态逻辑证明义务的证明。演绎组件是一个基于JAVA动态逻辑的交互验证系统，J AVA动态逻辑是专门为JAVA程序的形式验证而设计的逻辑[3]。2.2JAVA CARD和JAVA CARD APIJAVA CARD是一种提供用JAVA编程语言（的子集）对智能卡进行编程的方法的技术 由于智能卡的资源有限，与完整的JAVA相比，J AVA C ARD语言在许多方面受到限制。 以下是JAVACARD不支持的功能列表：大型原始数据类型（int，long，double，float），字符和字符串，多维数组，动态类加载，线程和垃圾收集。大多数剩余的JAVA特性，特别是面向对象的特性，如接口、继承、虚方法、重载、动态对象6D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）创建由JAVA CARD语言支持JAVA CARD API是一个处理智能卡特定功能的库，如应用协议数据单元（APDU-用于卡与世界其他地方之间的通信），应用标识符（AID），JAVA CARD特定系统例程，PIN码等。JAVA CARD API 2.2中包含的一些软件包如下：• lang-提供了一些类，这些类是设计JAVA编程语言的JAVACARD技术子集的基础。此包中的类派生自标准JAVA编程语言中的java.lang，并表示JAVACARD虚拟机所需的核心功能。• 框架-提供了一个类和接口的框架，用于构建、通信和使用JAVCARD小应用程序。 这些类和接口提供了JAVA CARD环境所需的最低功能。这个包中的关键类和接口是：AID-封装与applet关联的应用程序标识符（AID）。· APDU-提供控制卡输入和输出的方法· Applet- 卡上所有JAVACARDapplet的基类它提供一种用于与小应用程序一起工作的方法，所述小应用程序将被加载到、安装到符合JAVCARD的智能卡上并在其上执行。· JCSystem-提供控制系统功能的方法，例如事务管理、瞬时对象、对象删除机制、资源管理和小应用程序间对象共享。Util-提供了使用数组和数组数据的方便方法。整个JAVA CARD API由57个类和接口组成，其中许多非常简单（例如异常类）。2.3JAVA CARD API的OCL规范用例关键系统的目的之一是正式验证JAVA CARD应用程序的可能性。要成功验证使用JAVA CARD API的程序，必须访问API的实现或其正式规范。由于API的实现通常是不可用的（特别是当方法是原生的时），后者是我们的目标解决方案。让我们看一个例子来说明如何在验证过程中使用JAVACARDAPI规范。 假设我们有在我们的JAVA CARD程序中实现了一个方法aMethod。我们现在要验证实现是否满足形式规范（··D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）7方法a的前条件和后条件）。/*** @preconditions前>* @postconditions post>*/public void online（.）{1}...API Class.apiMethod（...）;...}我们的方法从JAVA CARD API调用一个方法，我们假设它已经被指定了。方法的指定及其实现被转换为证明义务，该义务又被传递到KeY演绎组件（证明器）。当试图为这个证明义务构造一个证明时，我们迟早必须应用一个规则来处理API方法apiMethod的调用。如果我们没有指定这个方法，我们将不得不用实际的方法来替换方法调用身体如果apiMethod的规范可用，则只需验证apiMethod的前提条件在apiMethod执行之前的状态中得到满足然而，这并不像听起来那么简单在KeY项目中正在进行的工作是调查何时以及在什么条件下可以安全地进行这样的替换[6]。除此之外，从长远来看，拥有API的OCL规范可以在验证JAVA CARD程序时节省大量工作。当没有可用的规范时，同一个API方法调用必须被方法的实现替换，并在每次使用该方法时进行证明。在实践中，可能会发生同一个API实现在一个程序中多次被放置在证明中为JAVA CARD API编写OCL规范的第二个目的是为了文档化-OCL规范可以作为JAVA CARD API的正式文档这是非常有用的，因为非正式规范并不总是包含有关API行为的所有必要信息。2.4相关工作如 前 所 述 ， 这 项 工 作 的 起 点 是 用 JAVA 建 模 语 言 （ JML ） 编 写 的JAVACARDAPI的正式规范[12，13，16]。这项工作是出于与上述类似的原因进行的，8D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）主要区别是使用的语言规范。[20]中提出的LOOP工具使用JML和PVS作为正式验证JAVACARD程序的方法，因此有必要使用JML编写API规范。由于我们在KeY项目中使用行业标准OCL作为规范语言，因此我们需要在OCL中制定JAVACARDAPI规范。我们亦作出修订，以在我们的规范中更全面地涵盖JAVACARDAPI。3OCL规范的发展如上所述，我们的规范基于JML规范的JAVA CARD API。然后，我们根据非正式规范（API文档）对其进行了扩展，并尽可能地利用OCL后来，我们通过正式验证（使用KeY系统）JAVA CARD API w.r.t.的部分参考实现来测试部分规范。我们的规格。我们首先给出JML的总体描述和JAVA CARD API的 JML在此基础上，我们将描述在为API编写OCL规范时需要解决3.1JML与OCL与OCL一样，JML中的规范表示为类不变式和方法前置/后置条件。类不变量是在任何时候都应该对类的所有实例保持有效的断言。前置条件和后置条件是方法的提供者和用户之间的契约。 用户在调用方法时必须满足前提条件。提供程序保证，如果在方法调用开始时前置条件保持不变，则相应的后置条件将在方法调用之后保持不变。此外，JML允许人们表达方法何时抛出异常，以及类的哪些所有JML规范仅在其JAVA源代码的上下文中有效，并以JAVA注释的形式呈现。下面是用于表达方法行为的JML的一般语法/**@公众行为@requires precondition>;@assignable list ofattributes>;@ensures postcondition>;@signals（Exception_1 e1）ex1postcondition>;D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）9@signals（Exception_2 e2）ex2postcondition>;*/public void onDestination（）{... 个文件夹@requires子句定义方法其余规范的含义如下：如果满足前提条件，则方法正常终止（即不抛出任何异常）并且后置条件（@ ensure）保持不变，或者抛出列出的异常之一，然后相应的后置条件保持不变。JML还允许在方法不应该抛出任何异常的情况下使用更简单的语法该示例给出了JML中的JAVACARDAPI规范的一般印象。下面是OwnerPIN类的publicclass PINs {private byte[] pin;private byte maxTries;private byte triesRemaining;public boolean check（byte[] thePin，short offset，bytelength）抛出ArrayIndexOutOfBoundsException，NullPointerException {...}...}pin数组包含PIN号码，maxTries是卡锁定前允许提供正确PIN的最大尝试次数，而triesRemaining是提供正确PIN的剩余尝试次数。这个类的JML不变式如下：/**@invariant triesRemaining >= 0&& triesRemaining = maxTries;*/下面给出了方法检查的JML规范arrayCompare方法比较数组this.pin的长度元素（从索引为0的元素开始）和数组thePin的长度元素（从索引为offset的元素开始）/**@public normal_behavior@requires triesRemaining > 0&&10D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）@Util.arrayCompare（this.pin，（短）0，@thePin，offset，length）==0; @确保结果==真triesRemaining==maxTries;*/在这一点上，我们已经准备好定义JML之间的主要差异。和OCL，这在用OCL编写JAVA CARD API规范KeY系统提供了对OCL的扩展，以克服大多数这些问题。3.2例外当前版本的OCL在其标准形式中没有提供一种直接的方法来指定异常是由方法引发的。一个可能的解决方案是在我们的类中有一个关联链接抛出，它表示该类的方法抛出的异常集。然后可以指定类MyClass的方法aMethod抛出一个excep，MyException类型的方法：context MyClass：：aMethod（）：pre：truepost：self. thrownlog->exists（e：Exception|e.oclIsKindOf（MyException）和e.oclIsNew（））KeyY系统对此有一个统一的解决方案-可以在后置条件中使用excThrown（My- Exception）稍后，当OCL规范被转换为证明者的JAVA动态逻辑证明义务时，exThrown子句被正确地转换为对应的JAVA动态逻辑公式。有了这些，我们现在可以给出OCL中JML的@be-observer子句的一般表示context MyClass：：aMethod（）pre：precondition>post：（不是excThrown（java：：lang：：Exception）和postcondition>）或者（exThrown（Exception_1）and）或者.or（excThrown（Exception_n）and exnpostcondition>）3.3空值在JAVA中常用的另一个东西，但在当前版本的OCL中不支持的是null值。这可以在OCL中处理，D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）11两种方式：• 当一个人想要将一个类属性与一个空值进行比较时，可以将该属性视为一个关联端，在OCL中可以将其视为一个集合。在这种情况下，可以简单地说attr->isEmpty（）来表示attr具有null值的事实。• 当比较对象而不是类属性（例如方法参数）与空值时，事情就有点困难了。如果这样的对象是数组或集合类型，则可以使用与上述相同的技术。否则，没有办法指定对象应该（或不应该）具有null值。幸运的是，KeY系统也为这个问题提供了一个解决方案。我们可以直接使用null值，就像它在OCL中定义的那样，然后在转换到JAVA动态逻辑的过程中，null值会得到适当的处理。3.4算术JAVACARD程序处理的主要数据类型是JAVAshorts、bytes和array。数组JAVA算术类型short和byteOCL中唯一的整数类型是整型。JAVAshorts和bytes最 重 要 的 一 点 是 它 们 可 以 覆 盖crowd （ 即 它 们 是 有 限 类 型 ） ， 而OCLcrowd是无限类型，永远不会覆盖crowd。由于过流行为是一个非常作为JAVA程序的一个重要方面，我们必须能够区分OCL中不同的整数类型。为此，我们使用了伪 他们可以 可以这样使用：context PIN：：check（pin：Sequence（JByte），offset：JShort，长度：JByte）：Boolean...这仍然没有解决在有组织犯罪法中如何正确解释过度贿赂的问题。幸运的是，钥匙系统再次拯救了我们。当OCL规范被转换为J AVA动态逻辑公式时，用户可以选择证明器如何解释整数类型：或者作为有限J AVA 类型short和byte，或者作为有限算术类型arithShort和算术字节在这两种情况下，都适当地处理了过度流动的问题更关于处理KeyY系统中的算术可以在[5，17]中找到还有，[8]给出了与JML中的整数算术相关的问题的见解。12D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）3.5可赋值子句如前所述，JML提供了一种可能性，即（使用@assign- able子句）允许给定方法在执行期间更改有限的属性集。OCL不提供任何机制或语言用一种很好的方式来指定它。当然，我们可以在后置条件中声明，给定属性的值不会被方法改变，方法是这样的：post：self.attr=self.attr@pre但这不是一个好的解决方案假设我们有一个有20个属性的类，我们想表达只有一个属性是可赋值的。这意味着我们必须为所有剩余的属性编写19个类似上面的表达式目前正在进行的工作旨在解决KeyY系统中的这个问题[6]。这项工作是关于如何正确指定属性修改行为以及如何在证明中使用这种指定。在我们工作的当前版本中，我们省略了与JML中@assignable4规格目前的工作导致了JAVA CARD API 2.2的所有类和接口的OCL规范除了少数例外（一些信号子句和可赋值子句无法在OCL中完全表达），该规范表达的内容与JAVA CARD API 2.1.1的JML规范一样多。在某些情况下，OCL规范比JML规范表达更多。下面我们通过例子来说明我们的OCL规范是如何创建的，以及它是如何改进的（与JML相比）。首先，让我们看看PIN接口（OwnerPIN实现的）。PIN接口中方法检查的非正式规范如下：public boolean check（byte[] pin，short offset，byte length）将PIN与PIN值进行比较。如果它们匹配并且PIN未被阻止，则它将设置已验证的标记并将尝试计数器重置为最大值。 如果不匹配，则递减尝试计数器，如果计数器已达到零，则阻止PIN。即使事务正在进行中，也不能有条件地更新内部状态，如尝试计数器、已验证的标记和阻塞状态。备注：• 如果引发NullPointerException或ArrayIndexOutOfBoundsException，则必须将验证的标记设置为false，必须递减try计数器，并且如果计数器达到零，则阻止PIN• 如果offset或length参数为负，则抛出ArrayIndexOutOfBoundsException• 如 果 offset+length 大 于 pin.length （ pin 数 组 的 长 度 ） ， 则 抛 出 ArrayIndexOut-OfBoundsExceptionD. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）13• 如果pin参数为null，则抛出NullPointerException主要参数：固定包含正在检查的PIN值的字节数组偏移引脚阵列中的起始引脚集长度销的长度回报率：如果PIN值匹配，则为true;否则为false投掷：ArrayIndexOutOfBoundsException，如果检查操作将导致访问数组边界之外的数据。NullPointerException如果pin为null。在[15]中找到的这种方法的JML规范如下（旧的构造对应于OCL/**@ 公众正常行为@requirestriesRemaining==0;@assignable\nothing;@确保结果==false;@也@ 公众正常行为@requires triesRemaining> 0&&pin！= 零&&偏移>= 0 @&&长度>=0&&偏移+长度==引脚长度&&@Util.arrayCompare（this.pin，（short）0，pin，@offset，length）==0;@ assignable已验证，triesRemaining;@确保结果==trueisValidated@triesRemaining==maxTries;@也@ 公共行为@requires triesRemaining> 0&&！(pin！= null&& @offset>= 0&&length>= 0&&@偏移量+长度==pin.length&&@Util.arrayCompare（this.pin，（short）0，pin，@offset，length）==0）;@assignable isValidated，triesRemaining;@确保结果==false&&@！isValidated&&triesRemaining ==@\old（triesRemaining）-1;@信号（NullPointerException）@！isValidated&&14D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）@triesRemaining == \old（triesRemaining）-1;@signals（ArrayIndexOutOfBoundsException）@！isValidated&&@triesRemaining ==\old（triesRemaining）-1;@*/public boolean check（byte[] pin，short offset，byte length）抛出ArrayIndexOutOfBoundsException，NullPointerException;JML规范似乎在JML规范中没有涉及的一个主题是下面的一句话：即使一个事务正在进行中，内部状态（如try counter、validated validate flag和blockingstate）也不能有条件地更新。 这在JML或OCL中都无法指定，因为它与J AVAC ARD EJB环境的内部事务机制有关。 在KeY项目[ 4 ]中，详细说明和验证涉及JAVACARD但是，现在我们决定在OCL规范中不考虑这个问题。 另一件需要注意的事情是，非正式规范和JML规范不一致 对 的 主题 的 是否 偏移量+长度必须 被 平等 销长度或如果offset+length可能小于或等于pin.length，似乎在JML规范中出现了一个错误，因为它显然与非正式规范不一致，而且似乎没有很好的理由要求在实际PIN值之后的引脚阵列中必须没有空闲元素。因此，我们得到的OCL规范与本例中的非正式规范一致：context PIN：：check（pin：Sequence（JByte），offset：JShort，长度：JByte）：Boolean前：真post：ifself.triesRemaining = 0 then result = false endif andif（self.triesRemaining > 0 and pin> null和offset>= 0和length>= 0和offset+length<= pin->size（）和self.pin->subSequence（1，长度）=pin->subSequence（offset+1，offset+length））那么（result= true和self.isValidated和self.triesRemaining = self.maxTries）endif如果（self.triesRemaining> 0和D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）15not（pin> null and offset >= 0 and length >= 0和offset+length = pin->size（）和self.pin->subSequence（1，length）=pin->subSequence（offset+1，offset+length））那么（不self.isvalidated和self.triesRemaining = self.triesRemaining@pre-1 and（（not excThrown（java：：lang：：Exception）and结果=false）或exThrown（NullPointerException）或excThrown（ArrayIndexOutOfBoundsException）））endif在下一个例子中，我们将展示DESKey类中setKey方法的规范与JML规范相比是如何丰富的。方法setKey复制作为参数传递的数据（字节数组），并构成内部属性数据的实际键。在某些情况下，此数据不是以纯文本形式传递给方法，而是作为密码，然后该方法必须在将数据复制到内部表示之前对其进行解密。以下是该方法的JML规范：/**@公众行为@requires keyData！= null&&kOff>=&&0@kOff= 0 andKoffsize（）post：（not excThrown（java：：lang：：Exception）andself.isInitialized（）and（not self.oclIsKindOf（javacardx：：crypto：：KeyEncryption）或self.getKeyCipher（）= null意味着16D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）））或（self.data->subSequence（1，self.getSize（）/8）=keyData->subSequence（kOff+1，kOff+self.getSize（）/8）excThrown（CryptoException）和CryptoException.systemInstance.reason= CryptoException.ILLEGAL_VALUE和（notself.oclIsKindOf（javacardx：：crypto：：KeyEncryption）或self.getKeyCipher（）= null意味着kOff+self.getSize（）/8> keyData->size（）））我们在此规范中添加的内容如下。如果DESKey的这个特定实例不是javacardx.crypto.KeyEncryption的实例，或者如果这个实例不与Cipher对象相关联（输入keyData必须被解密的情况），那么输入数据将被直接复制到内部属性数据中。在研究JML 规范时，我们发现了少量的错误不一致。例如，在OwnerPIN类中，不变式声明内部类属性pin在任何时候都不应为null，这要求该类的构造函数将pin（初始值为null）设置为非空值。在这种情况下，构造函数应该能够修改pin属性，但是在OwnerPIN构造函数的规范中缺少相应的@assignable该构造函数的非正 式 规 范 还 指 出 ， 可 以 抛 出 两 个 异 常 -PINException 和SystemException。抛出PINException的条件有明确的定义，但是这个信息没有包含在构造函数的规范中我们试图弥补OCL规范中的所有这些小缺陷，并尽可能多地表达，但是，正如我们之前提到的，目前不可能在OCL中给出 JAVA CARD API4.1正式验证为了对我们的规范进行测试，我们研究了随SUN的JAVA C ARD开发工具包版本2.1.1 [ 18 ]分发的J AVA CARD我们试图验证这个实现w.r.t.我们所写的规范。 由于KeY系统的当前限制，这并没有达到人们所希望的程度。其中一个技术原因是，KeyY系统不处理D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）17我们使用的版本。由于数组几乎存在于JAVCARD API的所有地方，这是一个主要障碍。然而，我们可以报告，javacard.framework包已验证。一个更复杂的问题-验证OwnerPIN类中的reset方法是一个成功的尝试具体如下：context OwnerPINinv：self.maxPINSize > 0和self.maxTries > 0和self.triesRemaining>=0self.triesRemaining = self.maxTriescontext OwnerPIN：：reset（）pre：truepost：not excThrown（java：：lang：：Exception）和not self.isValidatedand如果self.isValidated@pre，则self.triesRemaining=self.maxTries其他self.triesRemaining = self.triesRemaining@preendif由KeY系统生成的证明义务声明如下：reset方法的执行保留不变式，并且如果在执行reset之前满足先决条件，则在执行reset要解释这个证明义务是什么样子的，需要更详细地介绍KeY系统中使用的JAVA动态逻辑。这将超出本文件的范围不过，我们应该说的一件事是，验证此规范的证明是自动执行的通过KeY证明器，将用户交互减少到绝对最小。5OCL的简短评估我们发现关于OCL有一些非常有用的东西。 首先，它实际上是一个行业标准，并且（部分）得到了一些CASE工具的支持（例如，我们在KeY项目中使用的Borland Together Control Center）。其次，OCL语言在某些方面似乎比JML更丰富，例如：集合类型操作的整个库使得表达序列（数组）类型的属性比在JML中容易得多另基于同样的原因，我们发现OCL更容易阅读和理解。18D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004）当涉及到JAVA特定的特性时，OCL被证明不如JML好。简单概括一下3.1节中最重要的发现：在OCL中没有标准的方法来表达方法抛出异常的事实，相比之下，OCL中只有一种（无限）整数类型。整个JAVA整数类型集，并且在OCL中没有JML在这方面，JML是一种比OCL。当然，这是因为JML是专门为JAVA设计的，而OCL主要是为UML设计的。6结论在本文中，我们介绍了我们为JAVA CARD API 2.2开发OCL规范的经验。尽管OCL存在上述问题，但我们设法在合理的范围内指定了整个JAVACARDAPI。该规范可在以下网址在线获取：http://i12www.ira.uka.de/~key/doc/2003/exjob.html这项工作的两个主要目的是帮助和支持在KeY系统中正式验证JAVA CARD程序，并以正式的方式记录JAVACARD我们通过正式验证JAVA CARD API与KeY系统的参考实现来测试我们的规范尽管如此，我们尝试的证明是成功的，并且是由KeY系统自动执行的。在不久的将来，KeY系统将覆盖整个JAVA CARD标准。 然后我们计划继续朝这个方向发展，根据我们的具体要求，对现实生活中的JAVA CARD案例研究进行正式验证。引用[1] Wolfgang Ahrendt，Thomas Baar，Bernhard Beckert，Richard Bubel，Martin Giese，ReinerHa？ hn le ， Wolfr amMenzel ， WojciechMostowski ， Andr easRoth ， St e enS ch l ager ，anddPete r H. 施 密 特 钥 匙 工 具 。 计 算 科 学 技 术 报 告 第 2003-5 号 ， 计 算 机 科 学 部 ，CHALMERSUNIVERSITY和GüOTEBORUNIVERSITY，GüOTEBOR，瑞典，2003年2[2] WolfgangAhrendt 、ThomasBaar 、Bernhar dBeckert 、 MartinGiese 、 Reine rHäahnle 、 WolframMenzel、Wojciech Mostowski和Peter H.施密特关键系统：集成面向对象设计和形式化方法. Ralf-Detlef Kutsche 和 Herbert Weber ， 编 辑 ， Proceedings ， Fundamental Approaches toSoftware Engineering（FASE），法国格勒诺布尔，LNCS 2306，第327-330页。施普林格，2002年。[3] 伯恩哈德·贝克特。 一种用于JAVACARD程序形式验证的动态逻辑。在I. Attali和T. Jensen，编辑，修订论文，JAVAon Smart Cards：Programming and Security，法国戛纳，LNCS 2041，第6-24页。Springer，2001年。D. Larsson，W. Mostowski / Electronic Notes in Theoretical Computer Science 102（2004