Lifted structural invariant analysis of Petri net product lines

Abstract

Petri nets are commonly used to represent concurrent systems. However, they lack support for modelling and analysing system families, like variants of controllers, different variations of a process model, or the possible configurations of a flexible assembly line. To facilitate modelling potentially large collections of similar systems, in this paper, we enrich Petri nets with variability mechanisms based on product line engineering. Moreover, we present methods for the efficient analysis of the place and transition invariants in all defined versions of a Petri net. Efficiency is achieved by analysing the system family as a whole, instead of analysing each possible net variant separately. For this purpose, we lift the notion of incidence matrix to the product line level, and rely on constraint solving techniques. We present tool support and evaluate the benefits of our techniques on synthetic and realistic examples, achieving in some cases speed-ups of two orders of magnitude with respect to analysing each net variant separately.