Systematic Evaluation and Usability Analysis of Formal Tools for System Design

Formal methods and supporting tools have a long record of successes in the development of safety-critical systems. However, it cannot be said that a single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of modelling language used, verification capabilities and other complementary features, and each development context has peculiar needs that require different tools. This is particularly problematic for the railway industry, in which formal methods are highly recommended by the norms, but no actual guidance is provided for the selection of tools. To guide companies in the selection of the most appropriate formal tools to adopt for their contexts, a clear assessment of the features of the available tools is required. To address this goal, this paper considers a set of 14 formal tools for system design, and presents a systematic evaluation of the tools and a usability analysis with practitioners. Results are discussed considering the most desired aspects by industry and previous related work. The focus is on the railway domain, but the overall methodology can be applied to similar contexts. Our study contributes with a systematic evaluation of formal tools and shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by other works. Instead, process integration support is the most relevant pain point for the majority of the platforms.