论文部分内容阅读
UML广泛应用于软件建模，但缺乏有效的模型检测的方法，使用形式化方法对UML模型进行分析，可以发现UML模型的设计问题，提高UML模型的质量。对象着色Petri网是一种拥有接口库所的模块化着色Petri网，既是一种图形化建模工具，又是具有严格的语法语义定义的形式化方法。通过引入事件托肯，改进了将UML模型转换为对象着色Petri网的方法，结合实例将UML状态图和协作图映射为对象着色Petri网模型。并用着色Petri网的方法和工具对模型讲行了分析．验证了模型的一系列性质．