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

An Approach to Scenario-Based Property Verification

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

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 of 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 Propositional Linear Temporal Logic） formulas. Finally, we accomplish the verification using the ＂Reverse-Labeling＂ algorithm. Both the processes of synthesis and verification can be completed automatically.