论文部分内容阅读
UML(Unified Modeling Language)作为事实上的面向对象建模标准语言,它的复杂性和庞大性是不可避免的,但是它也包括了大量的具有模糊、稀疏语义的标准元素。在UML规范中,编制者是用较为形式化的语言OCL(Object Constraint Language)和自然语言两种手段描述静态语义,而动态语义却基本上完全是用自然语言来描述的,UML缺乏一个严格的动态语义定义。因此,对UML进行形式语义研究,对增进该语言的清晰性、等价性和一致性、可扩展性是十分有帮助的,为模型的正确性证明、转换以及支持UML建模工具的一致性检查提供了有力的理论工具。 目前,很多机构和个人都在从事UML的形式语义研究,他们试图通过对UML的研究来对UML的未来产生影响。这些机构和个人所采用的方法主要是补充法和具有面向对象扩展的形式语言方法。这两种方法各具有优点,但是也存在不足。在补充法中所使用的形式化语言不具有面向对象的特征,不能很好地和当前实践相结合,而具有面向对象扩展的形式语言方法又不能直接对UML模型的语义进行形式化,影响了读者对UML模型形式化的理解。 针对以上不足,作者将上述两种方法结合起来,提出了一种新的形式化状态机语义的方法,即首先对UML状态机的元模型的语法结构进行分析,然后通过具有面向对象特征的RAISE(Rigorous Approach to Industry Software Engineering)的说明语言RSL(RAISE Specification Language)直接对UML状态机的操作语义进行形式化。其中在对语法结构分析这一部分中,作者通过提出一个状态层次结构对UML状态机的各种状态及其间的相互关系进行分析,然后依次对事件、转换的结构进行分析,最后对UML状态机的语法结构进行了总结性形式化描述。在对UML状态机的“运行到完成”这一基本操作的语义进行形UML状态机的形式化语义研究式化中,作者运用RSL语言,依次对转换的成立、转换的冲突、冲突的解决、转换的选择的语义进行了形式化描述,并最终提出一个UML状态机“运行到完成”操作的算法。通过上述这两部分的结合,从而提出了一个完整的UML状态机语义形式化的新方法。. 最后,作者通过一个实例说明UML状态机语义的形式化描述可以证明那些用UML描述的系统的一些重要属性是正确的。