一种基于场景的性质验证方法

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

An Approach to Scenario-Based Property Verification

Sequence diagram is one of the most important mechanisms in UML, which can be used to model the dynamic behaviors of a system. Due to the difficulty o  f verifying whether the model satisfies some given properties, we propose an approach to such verification. First, we synthesize a sequence diagram and   its related stateehart diagrams into the PLPS （Proposition-Labeled Path Set） . Second, we describe the given properties using the FPLTL（Finite Propos sitional Linear Temporal Logic） formulas. Finally, we accomplish the verification using the ＂Reverse-Labeling＂ algorithm. Both the processes of synth hesis and verification can be completed automatically.