基于答案集程序设计的uml模型图推理方法

《基于答案集程序设计的uml模型图推理方法》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、计算机科学２００８Ｖ０１．３５ＮＱ．１１（专刊）基于答案集程序设计的ＵＭＬ模型图推理方法＊）邓文俊粱意文（武汉大学计算机学院武汉４３００７２）摘要使用ＵＭＬ模型图研发大型软件系统时，自动验证Ｕ胤模型图的正确性十分重要。但现有的验证方法都局限于一个或两个ＵＭＬ模型图。提出一个可自动验证多种ＵＭＬ模型图正确牲的方法。基于答案集程序设计，提出了将ＵＭＬ模型图和模型图的属性转换成逻辑程序的方法。通过验证眦模型图的属性在该逻辑程序的答案集语义中是否为真，来判断ＵＭＬ模型图的正确性。与现有的方法比较，本文的方法更具有普适性，适用于所有的Ｉ舢．模型图。关键

2、词ＵＭＬ，推理，答案集编程ＲｅａｓｏｎｏｎＵＭＬＤｉａｇｒａｍｓｗｉｔｈＡｎｓｗｅｒＳｅｔＰｒｏｇｒｍｍｎｉｎｇＤＥＮＧＷｅｎ－ｊｕｎＬＩＡＮＧＹｉ—ｗｅｎ（ＳｃｈｏｏｌｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ，ＷｕｈａｎＵｎｉｖｅｒｓｉｔｙ，Ｗｕｈａｎ４３００７２，Ｃｈｉｎａ）ＡｂｓｔｒａｃｔＴｏｓｕｐｐｏｒｔｔｈｅｄｅｓｉｇｎｏｆｌａｒｇｅ－ｓｃａｌｅｉｎｄｕｓｔｒｉａｌａｐｐｌｉｃａｔｉｏｎｓ。ａｕｔｏｍａｔｅｄｖｅｆｉｆｙｉｎｇｏｆｔｈｅＣ０１Ｔｅｃｔｎ骼ｓｏｆＵＭ旺一ｄｉａｇｒａｍｉｓｎｅｃｅｓｓａｒｙ．Ｈｏｗｅｖｅｒ，ｅｘｉｓ

3、ｔｉｎｇｍｅｔｈｏｄｓｌｉｍｉｔａｕｔｏｍａｔｉｃｖｅｒｉｆｉｃａｔｉｏｎｐａｐｅｒｐｒｏｐｏｓｅｓａｍｅｔｈｏｄｏｆａｕｔｏｍａｔｅｄｒｅａｓｏｎｉｎｇｏｎＩＭ，ｄｉａｇｒａｍｓｗｉｔｈＡｎｓｗｅｒＳｅｔｔＯｏｎｅｏｒＰｒｏｇｒａｍｍｉｎｇ（ＡＳＰ）．Ｆｉｒｓｔｏｆａｌｌ，Ｉ舢．ｄｉａｇｒａｍｓａｎｄｆｏｒｍａｌｐｒｏｐｅｒｔｉｅｓｏｆＵＭＬｄｉａｇｒａｍｓａｒｅｒｅｐｒｅｓｅｎｔｅｄｗｉｔｈｌｏｇｉｃｐｒｏｇｒａｍｓ．Ｔｈｅｎｔｈｅｓｅｍａｎ－ｔｉｃｓｏｆｔｈｅｌｏｇｉｃｐｒｏｇｒａｍｓａｒｅｃｏｍｐｕｔｅｄ．Ａｆｔｅｒｔｈ

4、ａｔ。ｃｏｒｒｅｃｔｎｅｓｓｏｆｔｈｅＵＭＬｄｉａｇｒａｍｓｃａｌｌｂｅｄｅｔｅｒｍｉｎｅｄｂｙｃｈｅｅ－ｋｉｎｇｗｈｅｔｈｅｒｔｈｅ１０９ｉｅｆｏｒｍｕｌａｓｏｆｔｈｅｐｒｏｐｅｒｔｉｅｓａｒｅｔｒｕｅｓｅｔｉｎｔｈｅｓｅｍａｎｔｉｃｓ．１引言自动验证ＵＭＬ模型图的技术是解决上述问题的方法。这个技术应包括两部分：其一，形式化的语ＵＭＬ模型已成为软件开发的实际标准模型语言。但是，由于ＵＭＬ语言缺少精确的语义，因此其描述的设计中常存在错误。例如，在图１中，类Ａ的设计存在问题［１］。原因是：在聚合（ａｇｇｒｅｇａｔｉｏｎ）关系的其中一端

5、的重数（ｍｕｌｔｉｐｌｉｃｉｔｙ）是‘１’。重数‘１’说明类Ａ的每个对象一定对应一个类Ｂ的对象。同时，类Ｂ是类Ａ的子类。由于聚集关系的传义，描述ＵＭＬ模型图及其属性。其二，推理方法，自动验证ＵＭＬ模型图的属性是否满足。已有一些研究［１．５］定义了ＵＭＬ模型语义或者提出了ＵＭＬ模型上的自动推理方法。Ｓｚｌｅｎｋ提出了ＵＭＬ类图的形式化定义以及类图的语义［１］。Ｂ．Ｌｉｔｖａｋ描述了一个算法，该算法能验证Ｕ１ⅥＬ序列图与状态图间的一致性［２１。Ｂｅｒａｒｄｉ提出了用描述逻辑（Ｄｅ—递性和不对称性，类Ａ的所有实例化对象，构成了ｓｃｒｉｐｔｉｏｎ

6、Ｌｏｇｉｃ）Ｃ６］实现在ＵＭＬ类图上的推理‘３Ｉ。一条无穷的对象队列。于是，类Ａ有无穷多个对象，所以类Ａ的设计存在问题。Ｏ．．●图１类图Ｘｉａｏｓｈａｎ等人给出了一个ＵＭＬ序列图的形式化定义［４］。杨静，张明义提出了ＵＭＬ需求模型一致性的形式化定义［５］。但是，以上方法大多只应用于一个或两个ＵＭＩ。模型图，这是因为在多个ＵＭＬ模型图上推理具有一定难度，需满足两个条件：１．使用高级的模型语言，例如一阶逻辑，描述ＵＭＩ。模型图及其属性。一个算法是不可能在所有ＵＭＩ。模型图上推理的。并且，该语言要既能描述静态模型，也要能描述动态＊）国家自然辩学基金

7、资助项目，编号：６０５７３０３８。邓文俊媳士生，研究方向为答案集程序设计的理论及应用；粱意文教授，博士生导师，研究方向为人工免疫学、智能计算等。・２２４・ｔｗｏｄｉａｇｒａｍｓ．Ｔ｝ｌｉｓＫｅ＂，ｏｒｄｓ眦，Ｒｅａｓｏｎ，Ａｎｓｗｅｒｐｒｏｇｒａｍｍｉｎｇ模型。ＵＭＬ模型图分为静态模型图（ｓｔｒｕｃｔｕｒａｌｄｉ－字的集合Ｓ，通过如下两个步骤，可以将Ｐ转化为不ａｇｒａｍｓ）和动态模型图（ｂｅｈａｖｉｏｒｄｉａｇｒａｍｓ）。２．该语言必须具有自动推理的方法。有些研究定义了一个ＵＭＬ模型图的语义，但由于没有自动推理的方含ｎｏｔ的逻辑程序Ｐ

8、５：１．删除所有规则体中含有ｎｏｔＬ；，Ｌ∈Ｓ的规则，法，因而不具有实用性。２．删除剩余规则中的ｎｏｔＬ，。答案集编程［７］（ＡｎｓｗｅｒＳｅｔＰ