Inhalt des Dokuments
|Stephan Mennicke, TU
|Thursday, October 24, 2013, 4 p.m., TU Hochhaus,
10th floor, room
Feature models provide a well-established formalism for tailoring product spaces of highly configurable applications. Thereupon, multi-view staged configuration approaches modular- ize feature models for separation of concerns and apply workflow modeling for scheduling configuration decisions. However, the complex, often oblivious and even cyclic logical depen- dencies among feature configuration decisions obstruct compositional semantics of feature model views thus spoiling intuitive modeling and rigorous analysis of staged configuration processes. In this paper, we consider workflow Petri nets (WPNs) as a formal operational model for staged configuration that makes explicit causal dependencies among feature selec- tions. For the internal separation into composable configuration stages we further adopt the principles of open workflow nets. As a result, we prove the soundness notion of WPNs to naturally coincide with fundamental correctness requirements to be verified for staged configuration processes such as satisfiability, liveness and absence of dead features. Concluding, we present a sample tool implementation and provide results of our evaluation concerning scalability properties.