论文部分内容阅读
复杂系统的建模往往需要进行严格的形式化分析和验证,而UML却是半形式化的,因为其语法结构虽然采用了形式化的规约,但其语义部分则是用自然语言描述的,缺乏精确的语义描述,因此会导致一些问题。为了在软件开发早期阶段对UML2.0序列图模型进行分析和验证,本文给出了基于UML2.0序列图的一种事件确定有限自动机模型的定义以及序列图到该自动机的转换算法。文中首先给出了UML2.0序列图,事件确定有限自动机在语法和语义上的形式化描述,然后提出了一种用事件确定有限自动机来描述每个对象在序列图描述的场景中所参与的事件序列的转换方法,并扩展到带有组合片段的UML2.0序列图,接着将该转换方法付诸算法实现,并给出一个实例进行分析,最后本文设计并实现一个序列图到自动机的转换工具,验证了将UML2.0序列图转换为事件确定有限自动机的可行性。