Feature Petri Nets

In software product line (SPL) engineering, formal modelling and verification are critical for managing the inherent complexity of systems with a high degree of variability. The number of products in an SPL can be exponential in the number of features. Therefore, the challenge when modelling SPL lies in analysing and verifying large, complex models efficiently, in order to ensure that all products behave correctly. The choice of a system modelling formalism that is both expressive and well-established is therefore crucial. In this paper we propose two lightweight extensions to Petri nets: Feature Petri Nets provide a framework for modelling and verifying software product lines; and Dynamic Feature Petri Nets provide additional support for modelling dynamic software product lines.nrpages: 99-106status: publishe