Generating a Petri net from a CSP specification: A semantics-based method

doi:10.1016/j.advengsoft.2012.02.006

Generating a Petri net from a CSP specification: A semantics-based method

2012-08-01

5

PRE

AI

DOI：10.1016/j.advengsoft.2012.02.006

原文链接

原文求助

摘要

En 中文

The specification and simulation of complex concurrent systems is a difficult task due to the intricate combinations of message passing and synchronizations that can occur between the components of the system. Two of the most extended formalisms used to specify, verify and simulate such kind of systems are CSP and the Petri nets. This work introduces a new technique that allows us to automatically transform a CSP specification into an equivalent Petri net. The transformation is formally defined by instrumenting the operational semantics of CSP. Because the technique uses a semantics-directed transformation, it produces Petri nets that are closer to the CSP specification and thus easier to understand. This result is interesting because it allows CSP developers not only to graphically animate their specifications through the use of the equivalent Petri net, but it also allows them to use all the tools and analysis techniques developed for Petri nets. (C) 2012 Civil-Comp Ltd and Elsevier Ltd. All rights reserved.

Keyword:

Concurrent programming

CSP

Petri nets

Semantics

Traces

Specification and Simulation

Generating a Petri net from a CSP specification: A semantics-based method

摘要

期刊

机构

引用论文