论文研究-基于Kripke结构的UML状态图的形式语义和自动证明 .pdf下载

基于Kripke结构的UML状态图的形式语义和自动证明，赵也非，杨宗源，给UML赋予形式化的动态语义，可以在软件生命过程早期，对系统进行自动推导和证明。把模型检测应用于UML，是在软件架构中引入形式化