
handle: 20.500.14243/321031
Using the CIF 3 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.
I.2.8 ARTIFICIAL INTELLIGENCE. Problem Solving, and Search. Control theory, Control Methods, D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Model checking, Controller Synthesis, Correctness-by-Construction, D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Formal methods, Supervisory Controller, Software Product Lines
I.2.8 ARTIFICIAL INTELLIGENCE. Problem Solving, and Search. Control theory, Control Methods, D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Model checking, Controller Synthesis, Correctness-by-Construction, D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Formal methods, Supervisory Controller, Software Product Lines
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 19 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
