基于UML和Petri网的建模及其验证

摘要

为了更好的建立系统模型,分析系统模型的性质,提出一种基于UML和Petri网的建模方法。用UML对系统进行可视化建模,利用Petri网对系统的动态行为进行建模,从不同的角度对系统进行建模,运用两种建模方法的优势,以及UML和Petri网之间的转化规则,实现两种模型的转换。最后把Petri网转化为Promela程序,用SPIN工具Petri网模型进行验证。