论文部分内容阅读
UML顺序图反映了系统中并发对象之间的消息交互及顺序，在软件建模中占有重要地位。该文对UML顺序图模型的自动验证方法进行了研究，在把UML顺序图转换为Promela语言后，使用模型检验器SPIN来验证系统设计模型是否满足某些关键性质需求。为了加强该方法的适用性，采用可扩展的标记语言XML文件格式定义顺序图模型的外部表示形式，该表示方法遵从OMG的XMI标准，从而使验证过程适用于不同的UML建模环境。