Synthesis of Petri Nets from Message Sequence Charts Specifications for Protocol Design

摘要

This paper presents a new approach to design communication protocols that uses Message Sequence Charts (MSCs) for the specification of scenarios and Petri Nets (PNs) as an intermediate model towards implementation. A protocol is first specified as a set of MSCs, each modeling a scenario. The relations among scenarios are expressed using PN semantics. Then, to support analysis and derive an optimized implementation, PNs are used to formally represent the event traces of the MSCs. We define consistency between a MSC specification and a PN, and present a pattern-based Covering Algorithm that generates from a MSC specification a consistent PN.