没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记115(2005)39-47www.elsevier.com/locate/entcsPVS1中UML模型和OCL约束的形式化Marcel Kyas和Harald Fecher2Institute for Computer Science and AppliedMathematicsChristian-Albrechts-UniversitüatzuKiel,Germany弗兰克·S de Boer and Joost Jacob de Boer和Joost Jacob雅各布3CWI阿姆斯特丹,荷兰Jozef Hooman和Mark van der Zwaag4荷兰奈梅亨大学计算机科学系Tamarah Arons和Hillel Kugler5魏茨曼科学研究所,以色列摘要对象约束语言(OCL)是为UML模型中对象和对象结构的属性指定而建立的语言。 它尚未被广泛采用的一个原因是在工业中,缺乏对OCL的适当和集成的工具支持。因此,我们提出了一个原型工具,它分析了语法和语义的OCL约束连同UML模型,并将它们转换成的语言的定理证明PVS。这为UML和OCL定义了一个形式化的语义,并使用UML建模的系统能够进行形式化的验证。我们处理有问题的事实,即OCL是基于一个三值逻辑,而PVS只基于一个二值逻辑。关键词:OCL,PVS,形式验证,形式语义,UML1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2004.09.02740M. Kyas等人理论计算机科学电子笔记115(2005)391介绍今天,UML [7,8]及其文本规范语言OCL [11,1]被广泛用作面向对象系统的规范和建模语言。有很多工具可以支持使用UML符号的系统开发,从简单的然而,还没有一个程序集成了UML类图、状态机和OCL规范的验证和确认。我们专注于高阶逻辑中的演绎验证。这允许验证可能处于有限状态的系统。我们将UML的符号(类图、状态机和OCL约束)翻译成PVS的输入语言[9]。然后,最初在OCL中给出的规范可以使用PVS进行验证。我们描述的编译器实现了对UML图的定义良好的子集的翻译,这对于许多应用程序来说是足够的这个子集由类图组成,类图只与多重性0或1关联,没有泛型类,状态机(状态机总是可以表示为具有相同行为的状态机,如[13]中所述)和OCL约束。OCL是一种三值逻辑,必须在PVS中编码,PVS基于二值逻辑,并且只允许全函数。OCL的三值性的原因此外,额外的真值仅通过将函数应用于其域之外的值而间接发生。将OCL的部分函数转换为PVS的方式决定了如何处理三值逻辑。我们的变换将一个部分函数限制在它的定义域上,从而产生一个全函数。[12]中报告的工作定义了PVS6中UML状态机的形式化,其中不包括OCL到PVS的翻译在[2]中,定理证明者Isabelle/HOL [6]提出了OCL的形式语义与我们的方法相反,部分函数已经扩展到全函数,1本工作的一部分得到了IST项目Omega(IST-2001- 33522)的财政支持,见http://www-omega.imag.fr,以及NWO/DFG项目EST-J(RO 1122/9-1,RO 1122/9-2)。2mailto:{mky,hf}@i nf orm at ik. 乌尼-基耶勒德3mailto:{frb,jacob}@cwi.nl4mailto:{hooman,mb z}@cs. 库恩nl5mailto:{tamara h,k ug ler}@ wis do m.w ei zm ann. a c.il6这具有被实施在的假正经程序,看到http://www.isot.ece.uvic.ca/download.html网站。M. Kyas等人理论计算机科学电子笔记115(2005)3941通过引入一个未定义的值。虽然这种方法允许验证Meta定理,但实际UML模型的验证w.r.t.它的OCL规范仍然需要额外的证明,证明所有的值都是定义的。2运行实例我们使用埃拉托色尼筛作为一个运行的例子。它使用Generator和Sieve这两个类进行建模(参见图1)。模型中只存在类Generator的一个实例(生成器创建Sieve类的实例。然后它以递增顺序发送新实例的自然数,参见图2。从Generator到Sieve的关联称为itsSieve。Fig. 1. 图2.过滤器实例的类图 生成器的状态机在创建时,Sieve的每个实例接收一个素数并将其存储在其属性p中。然后它创建一个后继对象,名为itsSieve7,并开始接收一个整数序列i。如果p整除i,那么这个实例什么也不做。否则,它将i发送到itsSieve。这种行为如图3所示。8图三. Sieve的状态机7图1中Sieve类与自身的关联称为itsSieve。图2中的触发器tm(20)将其反应延迟20个时间单位。42M. Kyas等人理论计算机科学电子笔记115(2005)39−我们想要证明的安全属性是p对于每个Sieve实例都是素数;这可以在OCL中形式化为:context Sieve inv:{2..(p-1)}->forAll(i)|p.mod(i)<> 0)这个约束指出属性p的值不能被2和p1之间的任何数i整除。 为了证明这一点,我们需要确定,由Sieve的每个实例接收的整数序列是单调递增的。我们之所以选择这个例子,是因为它很短,但仍然很难验证。它涉及对象创建和异步通信,因此没有有限的状态空间。此外,模型的行为取决于对象之间发送的数据,还要注意,我们想要在模型上证明的属性是数论属性,即生成的数字是素数。这使得使用自动技术(如模型检查)无法显示所考虑的属性。3PVS中的表示我们考虑的UML图是类图和状态机的受限形式,它们都可以包含OCL表达式。3.1类图为了形式化PVS中的类图,我们定义了一个Class类型,它枚举了模型中出现的所有类的名称,以及一个关于类的谓词,它声明类是否是活动的。常量rootClass表示提供模型中第一个对象的活动类。此外,每个类的属性、操作、信号和引用名称都被枚举为一个类型。一个名称与其定义类的关联是通过将名称与相应的类名前缀来完成的。图1中所示的类图的转换如图4所示。对象和对象结构总是使用解释函数从这些定义中获得的我们假设一个PVS类型Object,其元素代表所有对象。函数class:[Object ->Class]作为-标志每个对象的类和函数状态:[Object -> [Attribute-> Value]]为每个对象分配其状态,这是所有属性的赋值。类型检查断言所有对象只使用为其类定义的属性,因此我们为对象类中未定义的属性分配一个M. Kyas等人理论计算机科学电子笔记115(2005)3943{⊥⊥类别:类型+={发电机,筛}active:pred[Class]= LAMBDA(c:Class):c = Generator OR c = Sieve;rootClass:(active)=GeneratorAttribute:TYPE+={Generatorx,筛z,筛p,unusedAttribute}参考:TYPE+={SieveitsSieve,发电机itsSieve,SieveitsGenerator,unusedReference}见图4。筛级图的翻译3.2状态机位置:类型+ =发生器61、发电机64、发电机66,筛25,筛28,筛32,筛33t28:转换=(#来源:= Sieve二 十 八 岁,trigger:= signalEvent(Sievee,筛z),guard:=(LAMBDA(val:估值):(不区分((val(p)),(val'aval(Sievez),actions:=(cons((emitSignal(SieveitsSieve,Sievee,(LAMBDA(val:Valuation):(val'aval(Sievez),空)),目标:=筛28,class:=nums(nums);transitions:setof[Transition]={t:Transition|t = t9 OR t = t11 OR t = t13OR t = t25 OR t = t28 OR t =t32 ORt =t34或 t =t37}图五.生成器状态机的翻译状态机被表示为图形,并且在状态机中出现的OCL表达式被转换为表示其语义的表达式。转换后的状态机的语义是根据使用类似于[5]中描述的函数的计算集给出的。例如,从状态1到状态1的转换(如图2所示,向下一个对象发送整数)被转换为图5所示的PVS片段。3.3OCLOCL是一个三值逻辑,它为每个公式分配一个值true、false或unfined()。这样做的原因是,每个部分函数f是def在OCL的语义中扩展为严格的全函数f=λx。如果x∈dom(f)thenf(x)else f,关系和谓词被解释作为三个真值的严格函数[11]。然而,OCL标准指出,只有当所有约束都为真时,模型才是良构的。由于我们有兴趣验证模型的正确性w.r.t.它的OCL规范,我们必须证明所有的OCL约束是真的,即,既不谎言,也不谎言。为了实现这一点,每个OCL公式都是直接转换为PVS,这样我们就可以将真值false和false等同起来。这种方法的优点是:(1)我们不需要要求每个函数的参数都是严格的。PVS通过自动生成类型一致性约束(TCC)来提供自己的方法来处理此问题。}44M. Kyas等人理论计算机科学电子笔记115(2005)39(2)我们不需要重新定义逻辑的核心,例如,and and意味着功能,在PVS中。相反,使用PVS为了将OCL的语义简化OCL中使用的一些原始函数是部分函数,可能会返回未定义的值,例如,除以零。在[2]中,Brucker等人通过显式地引入未定义值并形式化底层的三值逻辑,将部分函数扩展为全函数,这更接近于OCL的语义。这种方法的缺点是,在三值逻辑中的推理失去了PVS我们的方法是将每个部分函数限制在它的定义域上,这使得它成为一个全函数。这就需要对每个原函数的定义域进行形式化。OCL中使用的许多函数在PVS中已经有了相应的算术函数。缺少的函数被我们定义为库中的总函数,具有适当的语义。OCL允许在表达式中使用用户定义的函数,这些函数可以使用let构造或使用已声明为无侧射的操作来引入。如果给出了用户定义函数的实现,我们计算一个基于从类层次结构计算的类型定义的签名。模型中的所有实例都由OclAny9类型的值标识。 它包含特殊的文字nil10,表示不存在的对象。 在PVS中,我们定义类型ObjectNotNil,包含所有现有对象不包括nil。对于模型中定义的每个类Class,我们引入一个类型ObjectClass并生成ObjectClass的子类型ObjectClassNotNil。如果类Class2 是Class 的直接子类,那么ObjectClass2 的超类型是PVS 中的ObjectClass。这编码了PVS中对输入类层次结构的通常解释,PVS中用户定义的操作的签名直接从原始签名中获得,除了第一个参数的类型总是self,变成ObjectClassNotNil,其中Class引用定义操作的类的名称。然后PVS生成TCC来断言所有参数都在函数的域中。 无法证明它们OclAny类是模型中所有类的超类,类似于Java[10]请注意,nil是定义良好的,表示任何空集合。M. Kyas等人理论计算机科学电子笔记115(2005)3945在大多数情况下,表明原始OCL表达式是假的或未定义的。OCL的形式语义与执行OCL约束有关一个递归函数的值是unfined,如果它的评估是发散的。这种语义可能适合于运行时检查,但它是不可实现的,因为终止问题通常是不可判定的。然而,在PVS中,每个递归函数的终止都必须由排名函数和终止证明来保证。因此,我们将OCL中的递归函数直接转化为PVS中的递归函数。用户必须自己定义PVS输出中的排名函数,因为OCL没有提供任何定义此类排名函数的方法OCL的语义将泛量化和存在量化的意义分别定义为合取的可能无限扩展。disjunc- tions.与allpark()操作一起,其直观含义是所有现有类实例的集合因此,表达式. allpark()->forAll(n| true)不会在OCL的语义中终止,因此,它的值是unfined。我们的翻译忽略了这种复杂性,并将量化表达式直接转换为PVS 表达式FORALL (n :int ):TRUE。这种方法的主要优点是规范更容易证明。通过这种选择,我们放松了翻译的合理性,因为翻译的约束在PVS中是可证明的,但其原始OCL约束是未定义的,尽管如此,我们还是倾向于我们的语义,因为它通常更好地反映了用户我们和其他许多人一样,严重怀疑OCL的设计者是否选择了正确的解释allpark()函数和量化。最后,编写OCL语义中未定义的规范的第三种方法是通过访问模型的对象图(或状态)中的未定义值,例如,通过访问数组边界之外的数组成员,访问该类中未定义(但已声明)的属性,或将对象重新类型化(强制转换)为其真实类型的子类型。在真正的编程语言中,这通常会导致运行时异常。我们假设底层的行为语义保证每个属性都被定义,并为其他情况生成合适的假设,因为我们主要对部分正确性感兴趣。46M. Kyas等人理论计算机科学电子笔记115(2005)394初步经验本文所描述的形式主义和方法已在原型中实现。我们已经测试了编译器,例如,验证面向对象的版本的“埃拉托塞尼筛”中描述的第二节二、我们证明了只有素数生成的安全性质。证明使用TL-PVS [10]。我们的编译器生成的转换关系的复杂性被证明是具有挑战性的。看来这种复杂性是UML语义所固有的。最困难的部分是对队列中的消息进行推理。对于筛子来说至关重要的消息一个接一个的概念,由于纯粹的技术原因很难处理。筛子的证明依赖于这样的事实,即没有信号被丢弃,并且信号以先进先出的顺序从队列中取出。这两个性质必须在PVS中指定为不变量并分别证明。11注意,如果两个属性中的一个不成立,那么筛子就不会满足它的要求。规格。我们的编译器的运行时间通常不到一分钟,但在任何情况下,它都是由在PVS中证明模型正确所需的时间决定的。OCL中的粗略规范不足以自动化整个验证过程。对于证明,表示不变量的状态机的状态的注释可能非常有用,因为这些必须被公式化为当前证明中的中间步骤。这种扩展需要语义表示的一些变化,因为由此产生的证明方法更类似于[ 3 ]中实现的Floyd引用[1] Boldsoft和Rational Software Corporation以及IONA和Adaptive Ltd.对UML 2.0 OCL RfP的回应(ad/2000-09-03),2003年1月6日。修订提交文件,版本1.6(ad/2003-01-07)。[2] 阿希姆·D Brucker和Burkhart Wol。提出了一种在I s a belle/H O L中的形式化OCL语义。InVictoorCeno,CesarMunoz,anddSofi'eneTashar,editors,TP-HOLLNCS。[3] 弗兰克·S de Boer和Cees Pierik。带注释的面向对象程序的计算机辅助规范和验证。在ArendRensink和Bart Jacobs编辑的FMOODSKluwer Academic Publishers,2002.[4] Willem-Paul de Roever,Frank Siepke de Boer,Ulrich Hannemann,Jozef Hooman,YassineLakhnech,Mannes Poel,and Job Zwiers. 并发验证。剑桥大学出版社,2001年。[11]这不是PVS的局限性,而是交互式定理证明的一般局限性。M. Kyas等人理论计算机科学电子笔记115(2005)3947[5] 约瑟夫·胡曼和马克·范德·兹瓦格。 一个用计时来交流反应对象的语义。在SVERTS,2003年。http:verimag.imag.fr/EVENTS/2003/SVERTS/PAPER S-WEB/13-HoomanZwaag.pdf.[6] 放大图片作者:Tobias Nipkow,Lawrence C.保尔森和马库斯·温泽尔。Isabelle/HOL -LNCS的2283号。Springer-Verlag,2002.[7] 对象管理组。 UML 2.0基础设施规范,2003年。[8] 对象管理组。UML 2.0 Superstructure Specification,2003。[9] S. Owre,J. Rushby,and N.史恩卡PVS:原型验证系统。在Deepak Kapur,编辑,CADE施普林格出版社。[10] 阿米尔·普努埃利和塔玛拉·阿伦斯TLPVS:基于PVS的LTL验证系统。在Nachum Dershowitz,编辑,国际验证研讨会论文集Springer-Verlag,2003.[11] 马克·里克特。验证UML模型和OCL约束的精确方法。博士的sis,联合国iverr sttBremen,2002年。[12] I. 你好。 一种用于U M L系统的PVS系统管理的方法。《计算机科学》,6(11):1088-1108,2000年11月[13] D'nielV'o。 一种基于改进的远程位置系统的通用数据库。 InA. Corradini,H. Ehrig,H.- J. Kreowski和G. Rozenberg,编辑,ICGTSpringer-Verlag,2002.
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.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)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)