Formal methods and supporting tools have a long record of success in the development of safety-critical systems. However, no single tool has emerged as the dominant solution for system design. Each tool differs from the others in terms of the modeling language used, its 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 in their contexts, a clear assessment of the features of the currently available tools is required. To address this goal, this paper considers a set of 13 formal tools that have been used for railway system design, and it presents a systematic evaluation of such tools and a preliminary usability analysis of a subset of 7 tools, involving railway practitioners. The results are discussed considering the most desired aspects by industry and earlier related studies. While the focus is on the railway domain, the overall methodology can be applied to similar contexts. Our study thus contributes with a systematic evaluation of formal tools and it shows that despite the poor graphical interfaces, usability and maturity of the tools are not major problems, as claimed by contributions from the literature. Instead, support for process integration is the most relevant obstacle for the adoption of most of the tools.
翻译:正式方法和辅助工具在开发安全关键系统方面有着长期的成功记录,然而,没有出现任何单一工具作为系统设计的主要解决办法,每个工具在所使用的示范语言、其核查能力和其他互补特点方面与其他工具不同,每个发展背景都有特殊需要,需要不同的工具;铁路行业尤其有问题,因为规范高度推荐正规方法,但没有为选择工具提供实际指导;为指导公司选择适合各自情况采用的最适当正式工具,需要明确评估现有工具的特征;为实现这一目标,本文件审议了一套13种正式工具,用于铁路系统设计,对此类工具进行系统评估,对一组7种工具进行初步使用性分析,涉及铁路从业人员,讨论的结果考虑了行业最希望的方面和早期的相关研究;虽然重点是铁路领域,但总体方法可以适用于类似的情况;因此,我们的研究对正式工具的特征进行了系统评估,表明,尽管对最薄弱的图形界面的支持,但用于铁路系统系统系统系统设计系统设计工具的可使用性和成熟性,它表明,对于整合而言,使用工具的最大障碍不是主要障碍,而是工具的成熟性,因为采用工具是来自最薄弱的图形界面支持,而最相关的工具的整合过程。