PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Reniers M. A., De Vink E. P. Supervisory controller synthesis for product lines using CIF 3. In: ISoLA'16 - 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Corfu, Greece, 10-14 October 2016). Proceedings, pp. 856 - 873. T. Margaria, B. Steffen (eds.). (Lecture Notes in Computer Science, vol. 9952). Springer, 2016.
 
 
Abstract
(English)
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.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-47166-2_59
DOI: 10.1007/978-3-319-47166-2_59
Subject Software Product Lines
Supervisory Controller
Controller Synthesis
Correctness-by-Construction
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Formal methods
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification. Model checking
I.2.8 ARTIFICIAL INTELLIGENCE. Problem Solving, Control Methods, and Search. Control theory


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional