OB(PN)^2: an object based Petri net programming notation

DOI10.1007/3-540-45397-0_8MaRDI QIDQ2761716zbMATH OpenFDO

Publication date 7 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2001/20010247

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computing methodologies and applications (68U99)

Review text

In this paper we present the object-based language \(OB(PN)^2\), together with its semantics, defined as a translation into a class of high-level Petri nets. This translation defines the semantics of a \(OB(PN)^2\) program as a net, which can be analyzed using existing reachability analysis tools. The \(OB(PN)^2\) language is an extension of \(B(PN)^2\) as defined by Best and Hopkins, and the semantics is inspired by the \(B(PN)^2\) semantics defined in terms of M-nets. The semantics is interesting from two points of view: it lays the foundations for the development of automatic verification methods of concurrent programs written in object-oriented languages, and it can be seen as a set of rules for the translation of object-oriented specifications written in an object-oriented specification formalism into Petri-nets. The translation relies on the CCS-like composition operators defined for M-nets. Each program construct is translated to a box (a special kind of net) or an operation for combining boxes. Thus in essence each program is translated into an expression in the algebra of boxes. For the entire collection see [Zbl 0976.68544].

Recommendations

Cited in

(2)

This page was built for publication: \(OB(PN)^2\): an object based Petri net programming notation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2761716)