基于对象着色Petri网的UML模型研究

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

Research on UML Model Based on Object Colored Petri Net

UML is widely used in software modeling which has a problem on model checking.By using formal method to analyze and check UML models,the design problems can be found in early phase so as to improve the quality of UML models.To solve the problems of model checking of UML models,introduces a high-level Petri net called object colored Petri net which is not only a graphical modeling tool but also a kind of formal method.And by invoking event token,a method of transforming UML model to object colored Petri net is improved when mapping UML statechart diagrams and collaboration diagrams to object colored Petri net.Then analysis and verification of the model are illustrated to verify a series of properties.