FMCAT: Supporting dynamic service-based product lines

We describe FMCAT, a toolkit for Featured Modal Contract Automata (FMCA). FMCAT supports the analysis of dynamic service product lines, i.e., applications consisting of ensembles of interacting services organized as product lines. Services are modelled as FMCA, with features identifying obligations and requirements of services. Service requirements can be either permitted or necessary, whereas the latter are further partitioned according to their criticality. A notion of agreement among service contracts is used to characterise safety. We show how FMCAT can be used to (i) specify dynamic service product line, (ii) efficiently identify all valid products, and to synthesise a safe orchestration of services for either (iii) a single product, or (iv) the whole service product line. FMCAT exploits the theory of FMCA to efficiently perform the above tasks by only visiting a subset of valid products, and it is equipped with a GUI.