Constructing Weakly Terminating Interface Protocols
conference paper
Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.
TNO Identifier
1032201
ISSN
03029743
ISBN
978-303227878-4
Publisher
Springer
Source title
Application and Theory of Petri Nets and Concurrency, 47th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2026, Hamburg, 22-26 June 2026
Editor(s)
Desel, J.
Kalenkova, A.
Kalenkova, A.
Place of publication
Cham
Pages
87-108
Files
To receive the publication files, please send an e-mail request to TNO Repository.