Modeling and Model Checking Software Product Lines

2008 
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 yes or no answer but the set of systems of the product line that do meet the specified properties.
    • Correction
    • Source
    • Cite
    • Save
    • Machine Reading By IdeaReader
    26
    References
    145
    Citations
    NaN
    KQI
    []