Software Product Lines with Design Choices: Reasoning about ...

Software Product Lines with Design Choices: Reasoning about ...

Software Product Lines with Design Choices: Reasoning about Variability and Design Uncertainty Michalis Famelis, Julia Rubin, Krzysztof Czarnecki, Rick Salay, Marsha Chechik 1 Software Product Line Basics Feature model, Domain model, Feature mapping Different feature configurations result in different variants PL models a set of related, but different products 1 2 2

Feature Model Washing Machine Product Line Heat excludes Domain Model Wash Heat Locking Heat Delay Delay [heatEnabled;delayEnabled]/ Heat Delay HeaterOn() Heat

Waiting Dry Heat Delay Heat Delay Delay / HeaterOff(); Heat wash.Start(); Heat Delay [not heatEnabled;not delayEnabled]/ wash.Start(); Heat / QuickCool() Unlocking Dry Washing

entry/TempCheck() Heat Dry Dry / QuickCool() Dry Dry Drying 3 Configuration Variant with Dry and Delay Domainwithout Model Model variability Wash Heat

Locking Heat Heat Delay Delay [heatEnabled;delayEnabled]/ Heat Delay Heat HeaterOn() Waiting Dry Heat Delay Heat Delay Delay

/ HeaterOff(); Heat wash.Start(); Heat Delay [not heatEnabled;not delayEnabled]/ wash.Start(); Heat / QuickCool() Unlocking Dry Washing entry/TempCheck() Heat Dry Dry / QuickCool() Dry Dry

Drying 4 Feature Model Evolving Washing Machines Decision point Mutex Not sure whether Heat and Delay are mutually exclusive Domain Model Heat Locking Heat Heat excludes Wash

Delay Delay [heatEnabled;delayEnabled]/ Heat Delay HeaterOn() Heat Waiting Dry Heat Delay Heat Delay Delay / HeaterOff(); Heat wash.Start(); Heat Delay [not heatEnabled;not delayEnabled]/ wash.Start(); Heat

/ QuickCool() Unlocking Dry Washing entry/TempCheck() Heat Dry Dry / QuickCool() Dry Drying Dry Decision point HasNoSpin Not sure whether to put a guard NoSpin on transition

5 Feature Model Design 1: No Mutex or HasSpin Heat excludes Heat and Delay not mutually exclusive Domain Model Heat Locking Heat Wash Delay Delay

[heatEnabled;delayEnabled]/ Heat Delay HeaterOn() Heat Waiting Dry Heat Delay Heat Delay Delay / HeaterOff(); Heat wash.Start(); Heat Delay [not heatEnabled;not delayEnabled]/ wash.Start(); Heat / QuickCool()

Unlocking Dry Washing entry/TempCheck() Heat Dry Dry / QuickCool() Dry Drying Dry No guard on the transition 6 Feature Model

Design 2: Mutex and HasSpin Heat excludes Heat and Delay mutually exclusive Domain Model Heat Locking Heat Delay Delay [heatEnabled;delayEnabled]/ Heat Delay HeaterOn() Heat Waiting

Dry Heat Delay Heat Delay Delay / HeaterOff(); Heat wash.Start(); Heat Delay [not heatEnabled;not delayEnabled]/ wash.Start(); Heat / QuickCool() Unlocking Dry Washing entry/TempCheck() Heat

Dry Dry Wash / QuickCool() Dry Drying Dry [NoSpin] NoSpin guard on the transition 7 Which one should we choose? A Design Space of SPLs

To explore this space, we need its properties {Mutex, HasNoSpin} {Mutex, HasNoSpin} {Mutex, HasNoSpin} {Mutex, HasNoSpin} 8 Software Product Lines with Design Choices Motivation How to model this design space? What are relevant properties for exploring it? How to check them? What to do when properties are violated? 9 Software Product Lines with Design

Choices (SPLDCs) 1 2 Design choices can affect the Feature model, Domain model, Feature mapping Decision combinations produce possible PLs They define a design space of product lines Given a space of product lines, which one should be selected (and why)? 1 2

Feature combinations produce possible products 10 Two Different Kinds of Choices Variability Design Uncertainty Reason Market demands for product variants Granularity Expression Semantics Features

Product line (PL) models Set of artifacts produced by combinations of features Long term Incomplete information, design alternatives, stakeholder conflicts, etc. Decisions Partial models Set of artifacts produced by combinations of decisions Short term Horizon 11 Modelling SPLDCs MUPotential candidates: MMINT Clafer: textual structural modelling language with

native variability abstractions PEoPL: product line implementation in Jetbrains MPS MU-MMINT: implementation of partial modelling in Eclipse Main challenges: Technological integration of tools Identification of usable syntax for intuitively expressing the two concerns 12 Software Product Lines with Design Choices Motivation How to model this design space? What are relevant properties for exploring it? How to check them? What to do when properties are violated? 13 A Design Space of Product Lines 1 2

Decision combinations produce possible PLs e.g., {Mutex, HasSpin} Goal: Use properties 1 to explore the design space of PLs 2 Feature combinations produce possible products 14

Constraining the Design Space using Properties For a product-level property P, we define four SPLDC-level properties using the modalities: Use All for critical properties and Some for desirable properties Use Necessary when you are sure it is needed and Possible when unsure but dont want to exclude the possibility All products have P Some products have P Necessary for the product line All products in All product lines Possible for the product line All products in Some product line Some product in All product lines

Some product in Some product line 15 Necessary-Some (NS) All product lines Some product 16 Possible-Some (PS) Some product line Some product

17 Possible-All (PA) Some product line All products 18 Necessary-All (NA) All product lines All product 19 Necessary-All (NA) Example product-level property: State Unlocking must

always be reached - a washing machine that violates this is unacceptable All product lines All product Example Analysis Check: does the SPLDC-level NA property hold? 20 Uncertainty in a Washing Machine Product Line Decision point Mutex Not sure whether Heat and Delay are mutually exclusive. Domain Model

Heat Locking Heat Feature Model Heat excludes Wash Delay Delay [heatEnabled;delayEnabled]/ Heat Delay HeaterOn() Heat Waiting Dry

Heat Delay Heat Delay Delay NO! / HeaterOff(); Heat wash.Start(); Heat Delay If and then the guard may prevent state Unlocking from Heat Washing being / QuickCool() reached. [not heatEnabled;not delayEnabled]/ wash.Start(); Unlocking Dry entry/TempCheck() Heat

Dry Dry / QuickCool() Dry Drying Dry Decision point HasNoSpin Not sure whether to put a guard NoSpin on transition. 21 SPLDC-level Properties SPLDC property modalities apply to any kind of product-level properties Behavioural (e.g., temporal logic) Structural (e.g., well-formedness constraints) Other (e.g., non-functional properties) The main challenge is in implementing the lifted analysis

such that it generates separate feedback for variability and design uncertainty 22 Generating Feedback for NA Property (Necessary-All) Counterexample product line Counterexample product 23 Software Product Lines with Design Choices Motivation How to model this design space? What are relevant properties for exploring it? How to check them? What to do when properties are violated?

24 Responses to Property Violation NecessaryAll? 25 Response 1: Relax Constraint NecessaryAll? Possible-All? 26 Response 2: Reduce Uncertainty NecessaryAll?

Reduce Uncertainty e.g., decide 27 Response: Reduce Uncertainty NecessaryAll? 28 Response: Reduce Variability NecessaryAll? Reduce Variability

e.g., remove feature 29 Response 3: Reduce Variability NecessaryAll? 30 Responding to SPLDC Property Violations Guidance for leveraging generated feedback: Should the problem be addressed at the SPLDC level? If so, which strategy is most appropriate? If not, can we recommend repairs? Sometimes we can address problems at the SPLDC level by addition E.g., adding previously forbidden configuration options Can we recommend such additions? FIXED! Necessary-Some (NS) violated:

31 Software Product Lines with Design Choices Motivation How to model this design space? What are relevant properties for exploring it? How to check them? What to do when properties are violated? 32 Current Work Focus on structural SPLDC properties SPLDCs as first-order theories Preliminary specification using Alloy Investigating more sophisticated reasoning engines (e.g. QBF, Second Order Logic) Next Steps Evaluating scalability of the tools and effectiveness of the methodology Better automation of response strategies Case studies

Power Window, Real Washing Machine, GitHub clones of configurable projects 33 Design Uncertainty and Variability Similar but different concerns Can be used together to model and explore a space of SPL designs We defined: Four natural classes of SPLDC-level properties that can be checked Strategies for responding to property violations 34

Recently Viewed Presentations

  • Comment'S on Sha Xin Wei'S

    Comment'S on Sha Xin Wei'S

    The array of detectors partition the continuous space of possibilities into a discrete (countable) set of experiencable parts. ... Example Continued: Entry of the quantum Zeno effect. Postulate that the felt effort causes, by virtue of the "fantastic laws of...
  • 33.1  Explain why we forget.  Herman Ebbinghaus was

    33.1 Explain why we forget. Herman Ebbinghaus was

    Retrieval Failure: although the information is retained in the memory store, it cannot be accessed.-Tip-of-the-Tongue: a retrieval failure phenomenon; given a cue, the subject says the word begins with the letter _. 33.1 - Explain why we forget.
  • About Internet2

    About Internet2

    Delivery of online services/content may be age- or grade-based Granularity of K12 organizational structure may be finer than HE IT Staffing, Skillsets in K12 frequently not focused on IAM/SAML 13-year relationship with moves between schools/districts Parents could easily have a...
  • Punctuation Pointers - Albemarle County, Virginia

    Punctuation Pointers - Albemarle County, Virginia

    Test: can you substitute who is? If so, use who's. If not, use whose. Who's/whose your daddy? It's hard to tell who's/whose on our side. Who's/whose pet python is that? Possessives vs. contractions: Who's/whose (almost to the end, I promise!)
  • IB Diploma Programme

    IB Diploma Programme

    IB Diploma Programme Information about the Diploma Zhuhai International School
  • Experience of Health Care Refo rm An overview

    Experience of Health Care Refo rm An overview

    GOOD SAMARITAN OVERDOSE ACT. Even in cases where immunities in subsection 12(1) do not apply, the Court, before sentencing, "shall consider in mitigation any evidence or information that the defendant, in good faith, sough medical assistance for a person in...
  • Friday 6th October

    Friday 6th October

    Personification 4) The daffodils nodded their yellow heads at the walkers. 5) The water beckoned invitingly to the hot swimmers. 6) The china danced on the shelves during the earthquake. 7) The car engine coughed and spluttered when it started...
  • Financial Management under NRHM: Sharing the experience

    Financial Management under NRHM: Sharing the experience

    Financial Management under NRHM: Sharing the Experience Rajesh Kumar Dy. Controller General of Accounts Ministry of Finance, GOI _____ Formerly part of FMG, MOHFW