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

• Type: Conference
• Year: 2008
• Where: FMOODS
• Authors: Alexander Gruler, Martin Leucker, Kathrin D. Scheidemann
• Keywords: FMOODS 2008, Formal Methods, Model Checking, Multi-valued Modal Kripke, Product Line