利用对象Petri网验证场景

Verification of Scenarios with Object Petri Nets

序列图表示的场景常被用于系统开发早期的需求获取与描述,但因其弱语义性而难以被验证。将序列图表示的场景转换为语义精细的对象Petri网模型OPDL,并通过其仿真环境OPMSE对其进行仿真,将场景描述的系统行为"展示"给需求开发者和用户,以此进行行为需求的验证。

Scenarios are used to describe behavior requirements at the early stage of systems development. But it is difficult to verify them because of their weak semantic. This paper uses an object petri nets model OPDL and its corresponding simulation environment OPMSE to serve as the verification tool for the key scenarios of information systems. Sequence diagrams which specify scenarios are transformed into the corresponding OPDL model. Then through OPMSE, the behavior which the scenarios imply is revealed to the modeler and the users, and thus the scenarios are verified.