Automated verification of feature model configuration processes based on workflow Petri nets

摘要: Modern software systems are highly configurable in order to satisfy diverse customer requirements and application contexts. Feature models provide a well-established formalism for tailoring configuration spaces of applications. Thereupon, multi-view staged approaches modularize feature separation concerns apply workflow modeling scheduling decisions. However, the complex, often oblivious even cyclic logical dependencies among decisions obstruct compositional semantics model views thus spoiling intuitive rigorous analysis processes. In this paper, we Petri nets (WPNs) as formal operational that makes explicit causal selections. For internal into composable stages further adopt principles open nets. It is shown soundness notion WPNs naturally coincides with fundamental correctness liveness properties be verified We present prototype implementation an automated computation processes experimental results concerning scalability properties.