Object-oriented modelling with high-level modular Petri nets

In this paper, we address the problem of expressing object-oriented concepts in terms of Petri nets. This is interesting, first, as a possibility of representing concurrent system specifications written in object-oriented formalisms or languages with Petri nets, and second, as a way of allowing automated verification of the obtained Petri net using existing reachability analysis tools. We start from an existing parallel specification language having a modular Petri net semantics and we extend it with object-oriented features inspired from Java and C++. The translation of these new extensions into the Petri net domain is given using a class of modular coloured Petri nets and includes, in particular, a treatment of inheritance and of dynamic binding.