ABSTRACT. The railway sector has seen a large number of successful ap- plications of formal methods and tools. However, up-to-date, structured information about the industrial usage and needs related to formal tools in railways is limited. Two Shift2Rail projects, X2Rail-2 and ASTRail, have addressed this issue by performing a systematic search over the state of the art of formal methods application in railways to identify the best used practices. As part of the work of these projects, question- naires on formal methods and tools have been designed to gather input and guidance on the adoption of Formal Methods in the railway domain. Even though the questionnaires were developed independently and dis- tributed to different audiences, the responses show a certain convergence in the replies to the questions common to both. In this paper, we present a detailed report on such convergence, drawing some indications about methods and tools that are considered to constitute the most fruitful approaches to industrial adoption.

ABSTRACT. This extended abstract a method to analyze software specification or implementation driven by the goal to construct a mathematical proof that the software guarantees key high-level properties. The application of the method is safeguarded by the use of tool-equipped formal methods and has been applied successfully to several industrial products.

ABSTRACT. The experiences had during the application of Event-B to a subsystem of a way-side train monitoring system (WTMS) will be presented in this paper. The WTMS configuration management system (CMS) supports the creation and management of configuration data for the WTMS. Consistency of system data is one of the most important quality properties of a CMS since inconsistency may lead to critical malfunctioning. Therefore, the development of the data handling part of a CMS requires the use of high-integrity methods in order to ensure the highest quality. Event-B with its set-theoretic basis for modelling, its notion of refinement and the use of formal proof ensuring consistency of refinement steps has been used for the conceptual modelling of system data and system operations. Due to the agile structured development process, the conceptual model has been created in several iterations by a changing team of developers. The challenge was to guarantee completeness and consistency of this model and to keep it aligned with the goals of all relevant stakeholders. This has been achieved by an incremental, refinement-based creation of a formal conceptual model along with an appropriate formalization of the conceptual data constraints. The relationship between the conceptual model and the formal conceptual model has been realized by an appropriate traceability model. This paper describes how the application of Event-B can successfully address these challenges.

ABSTRACT. This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended use of OpenUxAS, there are many safety and security implications; however, these considerations are unaddressed in the current implementation. AFRL is seeking to address these considerations through the use of formal methods, including through the application of SPARK, a programming language that includes a specification language and a toolset for proving that programs satisfy their specifications. Using SPARK, we reimplemented one of the core services in OpenUxAS and proved that a critical part of its functionality satisfies its specification. This successful application provides a foundation for further applications of formal methods to OpenUxAS.

ABSTRACT. The usage of formal methods in Model Driven Engineering (MDE) has already been demonstrated with a significant boost in both productivity and quality in the design and analysis of software and systems. However, the integration of appli-cable tools and techniques for formal analysis needs improvement in order to cre-ate a practical MDE environment for FM, suitable for use in an industrial setting. This paper presents the European Space Agency (ESA) MORA-TSP (Multicore implementation of the On-Board Software Reference Architecture with Time and Space Partitioning capability) study. MORA-TSP comprises to develop a MDE toolset suitable to apply FM for early analysis, correctness and validation of the modeled software, in the context of space flight software.