附件论文：

基于pi 演算的UML 状态图的组装机制以及模型精化的验证

 

摘要：UML 提供了面向对象的、图形化的方法，可以描述系统模型的各个方面。但是，UML 是一种元模型，只有静态语义，不具备动态语义。本文从组装方式的角度出发，总结并提出了6 种UML 状态图的组装机制，并赋予了相应的pi 演算语义，给出了映射规则，最后用实验和理论推导两种方法，证明了该理论可以验证模型精化。通过给UML 赋予形式化语义，可以实现自动的分析、推理、验证；通过提出6 种组装方式，可以建模系统的静态拓扑和动态行为。

发表期刊：科技论文在线（评为精品论文） 

发表日期：2008年9月

转载本文请联系原作者获取授权，同时请注明本文来自赵也非科学网博客。
链接地址：https://blog.sciencenet.cn/blog-107188-207880.html

上一篇：基于Kripke结构的UML状态图的形式语义和自动证明
下一篇：基于SMV 的滑动窗口协议的形式化建模与分析