Formal Methods Applied in Industry - On the Commercialisation of the UPPAAL Tool

UPPAAL is a model-checking tool primarily aimed for real-time and embedded systems in which timing plays an important role. It has existed for over 16 years and has become very popular among formal method scientists in academia. In recent years, licenses of the tool have also been offered and sold on commercial basis. In this paper, the characteristics of the tool, its domains of application, as well as some lessons learned from commercializing the tool are described.