Paper Info
Title
Modeling and Model Checking Software Product Lines
Abstract
Software product line engineering combines the individual developments of systems to the development of a family of systems consisting of common and variable assets.In this paper we introduce the process algebra PL-CCS as a product line extension of CCS and show how to model the overall behavior of an entire family within PL-CCS. PL-CCS models incorporate behavioral variability and allow the derivation of individual systems in a systematic way due to a semantics given in terms of multi-valued modal Kripke structures. Furthermore, we introduce multi-valued modal μ-calculus as a property specification language for system families specified in PL-CCS and show how model checking techniques operate on such structures. In our setting the result of model checking is no longer a simple yesor noanswer but the set of systems of the product line that do meet the specified properties.
Year
DOI
Venue
2008
10.1007/978-3-540-68863-1_8
FMOODS
Keywords
Field
DocType
individual system,pl-ccs model,entire family,model checking technique,individual development,model checking,product line,product line extension,model checking software product,software product line engineering,process algebra pl-ccs,process algebra
Transition system,Abstraction model checking,Model checking,Computer science,Theoretical computer science,Property Specification Language,Software,Software product line,Process calculus,Modal
Conference
Volume
ISSN
Citations 
5051
0302-9743
93
PageRank 
References 
Authors
2.52
15
3
Name
Order
Citations
PageRank
Alexander Gruler11588.30
Martin Leucker21639112.68
Kathrin Scheidemann31103.27