摘要：顺序图是UML中重要的语法机制，用于对系统的动态行为进行建模。但是，建模后模型是否满足某方面性质却很难检验。为此，我们提出了一种基于场景的性质验证方法。该方法首先把描述一个场景的顺序图以及相关的状态图综合成一个“命题标记路径集”，把待验证的性质表示为有穷线性时序逻辑公式，然后利用“逆向标注”算法对其进行验证。转化及验证过程均可自动完成。

关键词：顺序图 状态图 场景 命题标记路径集 有穷命题线性时序逻辑 

单位：长沙大学计算机系; 湖南长沙410003; 国防科技大学计算机学院; 湖南长沙410073