寻找中间语言 生成比较模型
在三位开发人员分别设计的用例图与类图中,其中一人在安防系统类图中定义系统参与者名称为“用户”,另一人在照明系统用例图中定义参与者名称为“使用者”,虽然二者的属性与操作都相同,但由于名称的不同,产生了名称上的不一致,这是需要通过检测去解决的问题。
在三位开发人员分别画的活动图与时序图中,存在相似的行为,在有相关需要时要对这些活动是否属于表现相同的行为做出合理的判断。例如需要判断安防系统活动图中从启动系统到监控家中情况的行为是否与时序图中设置安防模式的行为属于同一过程。
UML中的静态图有:用例图、类图、对象图、组件图、配置图等等。这些静态图描述的均为系统中的静态关系。相应的,在DIKW图谱中,D图谱体现的是各个节点以及它们之间的关系,它们的结构存在相异的表达方式。D图谱中节点间的关系是静态的,这能够与UML静态图中的关系相对应,所以,可尝试比较UML的静态图与DIKW中的D图谱。
UML中的动态图包括:时序图、协作图、状态图、活动图等。UML动态图刻画的均是动态关系。类似的,DIKW中的I图谱体现的是节点间的动态交互、行为关系,并且I图谱中所有元素都可以在D图谱里找到对应的类。因此,尝试将UML的动态图与DIKW中的I图谱进行对照。
为了寻找通过图谱帮助解决UML建模过程中一致性问题以及相同行为问题判断的方法,在查阅一致性检测的相关文献后,了解到关于单一的UML时序图的一种一致性检测方法为:可以将UML视图(时序图)通过XML转换器转换为中间语言,再通过SMV(符号模型验证器)程序产生器将中间语言转变为布尔公式与时序逻辑。接着,将转变得到的相关布尔公式与时序逻辑输入到NuSMV(模型检测工具)中,最后通过判断比较对象的执行踪迹是否与参考对象的事件序列保持一致,比较得出最终结论。
基于前面的分析,在此提供一种判断UML动态视图中的行为是否相同的思路:通过对UML动态图的定义与描述,提出从UML动态图到SMV的转换规则,包括每个动态行为的前后置条件以及行为中的不变量。首先将UML时序图与活动图转换为XML格式文件,再通过SMV程序产生器,将XML转变为布尔公式与时序逻辑的模型,以待进一步的检测。 类似的,通过对DIKW图谱中的I图谱的定义与描述,提出从I图谱到SMV的转换规则。接着将I图谱转换为XML格式文件,再通过SMV程序产生器,将XML转变为布尔公式与时序逻辑,作为待检测的模型。 最后,将待检测模型输入到模型检测工具中进行一致性检测,以判定UML动态图中的行为是否相同。
具体流程如下图所示:
第一步:用ArgoUML完成UML中的用例图、类图、活动图、时序图的构建;用Visio完成D图谱、I图谱的构建。这些图已经在论文第二章中做出展示;
第二步:将UML中用例图、类图、活动图、时序图以及图谱中的D图谱与I图谱导出为XML文件,并进一步基于规则将XML文件转变为布尔公式与时序逻辑;
第三步:将获取到的布尔公式与时序逻辑作为模型检测工具的输入,通过对比检测出UML建模过程中部分图的不一致问题。在整个检测过程中,将D图谱与I图谱作为参考对象。