A collection of models of a bike-sharing case study.

Bike-sharing systems are gaining popularity not only as a sustainable means of smart transportation in urban environments, but also as a challenging case study that offers interesting run-time optimization problems. As a case study within Quanticol, we have observed how such systems possess a wide variety of different features. We have therefore applied variability analysis to define a family of bike-sharing systems, covering the specification of a discrete feature model, specification of several non-functional quantitative properties, and behavioural specifications. Subsequently, we have sought support in available tools, establishing a tool chain of (academic) tools each covering a different aspect of the system, from feature modelling to product derivation and from quantitative evaluation of the attributes of products to model checking value-passing modal specifications. The tool chain was experimented to complement more sophisticated product-based analyses. This technical report collects the complete specifications of the models that were used in the tool chain.