附件论文： 基于Kripke结构的UML状态图的形式语义和自动证明

摘要：给UML赋予形式化的动态语义，可以在软件生命过程早期，对系统进行自动推导和证明。把模型检测应用于UML，是在软件架构中引入形式化方法的一个重要方向。本文使用UML状态图表示变量值的迁移，而非系统状态的迁移，以处理不能穷举系统有限状态自动机的情况；显式的提出了UML状态图和Kripke结构语义的映射关系；最后，用实验验证了该理论的有效性。本文提出的映射规则是双射的，因此，既可以应用于设计阶段的软件正向工程，又可以应用于实现阶段的逆向软件工程。

发表期刊：科技论文在线

发表日期：2008年12月