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

Abstract:

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.

Key words: sequence diagram, statechart diagram, scenario, proposition-labeled path set, finite propositio , anl linear temporal logic