Service-oriented systems involve synchronous, asynchronous, and recursive service calls. Existing research has identified limitations in Petri net-based approaches for deadlock detection, particularly in scenarios involving recursive calls. This extended abstract establishes a basis for evaluating the suitability of recursive Petri nets for modeling such interactions and for identifying deadlocks, with an emphasis on recursion-induced cases. The results are expected to demonstrate that the selected modeling approach substantially influences the accuracy of deadlock analysis in service-oriented systems.
Definition 1 (Marked Recursive Petri Net). A marked recursive Petri net (with initial extended marking and final extended markings) is the quadruple ⟨, 0, , ⟩, where (i) ≜ ⟨, , − , +, Ω ⟩ is a recursive Petri net (ii) 0 ≜ ⟨0, 0, 0, 0⟩ is an initial extended marking of (iii) ≜ { | = ⟨ , , , ⟩} is a set of final extended markings of and (iv) ≜ ⟨, , , ⟩ is an extended marking of reachable from 0 by 0→− , = 12 · · · .
The firing of a transition ∈ , →− ′ results in a marked recursive Petri net ⟨, 0, , ′⟩, provided that ̸∈ . If ∈ , execution halts regardless of any enabled transistions. Note that an initial marking refers to Ω( ) for ∈ , whereas an initial extended marking refers to 0. as a thread [4]. A deadlock that is local to a thread () is therefore termed a threadlock.
For each vertex ∈ in an extended marking of , the associated marking () is referred to ()() < − (, ).
Definition 2 (Threadlock). Let ⟨, 0, , ⟩ be a marked recursive Petri net with the current extended marking ≜ ⟨, , , ⟩ and ̸∈ . A thread () of vertex ∈ in the extended marking is in a threadlock, if no transitions ∈ are enabled in (), i.e. ∀ ∈ : ∃ ∈ : by (). A deadlock in a recursive Petri net can thus be constructed from individual threadlocks.
A threadlock also constitutes a deadlock in the underlying Petri net ¯ ≜ ⟨, , − , +⟩, marked () is in a threadlock.
Definition 3 (Deadlock in a RPN). Let ⟨, 0, , ⟩ be a marked recursive Petri net, let ≜ ⟨, , , ⟩. The marked recursive Petri net is in a deadlock for if ̸∈ and for all ∈ ,
Based on these two types of deadlocks, the abstraction from the service-oriented language is described, as illustrated in Tables Table 1a and Table 1b. For each control flow element shown in the left column, the corresponding recursive Petri net fragment is depicted in the upper part of the right column, while a sequence of extended markings is presented in the lower part. To simplify the notation, threads () are expressed using process-algebraic expressions of class according to Mayr’s hierarchy [3], where place names are separated by the commutative and associative operator ‖.
The number of occurrences of a place in a process-algebraic expression corresponds to the number of tokens in that place, representing asynchronous execution in a (, ) − . The places and are introduced to ensure that not all tokens from previous places are held until a final transition in the child thread fires. As a result, an asynchronous procedure call cannot be modeled using an abstract transition alone. Since recursive Petri nets are bipartite graphs, direct edges between transitions are not permitted; places and must be inserted accordingly.
This extended abstract presented an abstraction-based approach to enable deadlock analysis in serviceoriented architectures. The approach builds on an established programming model introduced in prior work [2]. A formal definition of deadlocks in recursive Petri nets (RPNs) was developed within the context of this abstraction. Existing counterexamples must be examined more thoroughly to support the validation of the proposed method. This will help assess whether the approach extends the expressive power of existing techniques, even in cases where certain deadlock scenarios—such as threadlocks—may remain undetected. Future work includes the identification and analysis of additional deadlock types in RPNs. Moreover, the ability of RPNs to model error handling is to be investigated. Prior studies have shown that correct modeling of exception handling is only achievable through (G,G)-PRSs [8]. It remains to be examined whether RPNs exhibit similar capabilities, potentially positioning them between PANs and (G,G)-PRSs within the Mayr hierarchy [3]. In addition, the backward inclusion relation between PANs and RPNs will be formally analysed to determine whether PANs form a proper subset of RPNs. Parallel to these theoretical investigations, tooling support for deadlock analysis in RPNs is under development, aiming to bridge the gap between theoretical insights and practical application.
, ( ′ ) ⟶ …
( ) (1b) Abstraction of asynchronous procedure call control flows to recursive Petri nets.
∶ ′ ∶ ∶= ; … 1 ∶ if { 2 ∶ 3 ∶ } else { 4 ∶ … … … … 5 ∶ } 6 ∶ …
Procedure : ∶ ′ ∶ ∶ ∶ () ; … () { } … return;
′ ⟶ ( ′) 1 2 2 4 ′ () ⋯ ⟶ ⟶ ⋯ ⋯ ⟶ ⟶3 ⟶ ⟶4 3 3 ⟶ ( ′) (1a) Abstraction of assignment, if-else and synchronous procedure call control flows to recursive Petri nets.
Declaration on Generative AI The author(s) have not employed any Generative AI tools.
2009, p. 5. open-source robot operating system, in: ICRA workshop on open source software, volume 3, Kobe,