TU Berlin

Referat für Kommunikation & MarketingVortrag Mennicke

Inhalt des Dokuments

zur Navigation

Gastvorträge 2013

Automated Verification of Feature Model Configuration Processes based on Workflow Petri Nets
Stephan Mennicke, TU Braunschweig
Thursday, October 24, 2013, 4 p.m., TU Hochhaus, 10th floor, room 1011


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.


Kristian Duske, Softwaretechnik



Schnellnavigation zur Seite über Nummerneingabe