Supervisory Controller Synthesis for Product Lines using CIF3
M.H. ter Beek, M.A. Reniers, and E.P. de Vink

Using the CIF3 toolset, we illustrate the general idea of controller
synthesis for product line engineering for a prototypical example of a
family of coffee machines. The challenge is to integrate a number of
given components into a family of products such that the resulting
behaviour is guaranteed to respect an attributed feature model as well
as additional behavioural requirements. The proposed
correctness-by-construction approach incrementally restricts the
composed behaviour by subsequently incorporating feature constraints,
attribute constraints and temporal constraints. The procedure as
presented focusses on synthesis, but leaves ample opportunity to
handle e.g.\ uncontrollable behaviour, dynamic reconfiguration, and
product- and family-based analysis.