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