Modelling and Analysis with Featured Modal Contract Automata

Featured modal contract automata (FMCA) have been proposed as a suitable formalism for modelling contract-based dynamic service product lines. A contract is a behavioural description consisting of offers and necessary and permitted service requests with different levels of criticality, to be matched with corresponding offers of other FMCA. Each contract is equipped with a feature constraint, whose features are offers or requests, and characterises a valid product orchestration. A safe orchestration of a product fulfils all necessary and the maximum number of permitted requests, such that all enabled features are available and none of its disabled features is. The entire product line orchestration can be computed from a subset of valid product orchestrations, by exploiting their (partial) ordering. The open-source prototypical toolkit FMCAT supports the specification and orchestration of FMCA, and it interfaces with FeatureIDE for importing feature models and their valid products. In this experience report, we show how to model a Hotel service product line with FMCA and how to analyse it with FMCAT.