This article presents an Event-B model and an interactive GUI prototype for an air traffic control system called the arrival manager (AMAN). AMAN is a safety-critical interactive system designed for air traffic controllers to manage landings at an airport. The presented formal model consists of a human-machine interface comprising interactive and autonomous parts. Safety properties of the system were proven using the Rodin platform, while validation was carried out using the ProB tool. We turned the formal model into an executable AMAN prototype by combining interactive domain-specific visualizations and automatic simulation using the VisB and SimB components of ProB . We used validation obligations (VOs) to systematically validate the model’s and the prototype’s compliance with the requirements and uncovered some contradictions and ambiguities in the case study.

In safety-critical engineering domains, engineering processes guide developers toward producing systems that adhere to stringent standards of safety and quality, while also allowing for the inherent flexibility of creative tasks. Process compliance focuses on ensuring that the engineering work-as manifested in the creation, tracking, and tracing of engineering artifacts-follows the described processes as closely as possible. The sequence of process steps is typically described using temporal process constraints over engineering artifact metadata (e.g., a requirement must transition from ‘draft’ to ‘ready for review’). Existing approaches, however, lack support for checking temporal constraints during development and rely on manual checks, resulting in delayed feedback when deviations occur. In this paper, we present an automated, incremental constraint checking approach that can evaluate temporal constraints across inter-related artifacts upon every artifact change, enabling timely feedback on process deviations. Our approach includes an incremental checking mechanism for temporal process constraints, and the ability to dynamically evaluate and integrate the history of artifacts as they become relevant for the constraints. Temporal constraints are expressed in the Object Constraint Language (OCL) extended with operators from Linear Temporal Logic (LTL). We demonstrate the ability of our approach to support a wide range of higher-level temporal patterns. We show that for constraints in an industry-derived use case, we can detect a significant number of temporal process constraint violations, some remaining unfulfilled after the end of the development process. We also find that, in this use case, the average evaluation for a single constraint operator takes around 0.3 milliseconds.

Abstract Context With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science. Objective We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019–2023) of research. Method Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources. Results This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented. Conclusions The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.

Refinement guarantees that the concrete version of a model does not violate the constraints introduced at the abstract level. The peculiarity of refinement, however, is that we have no guarantee about the preservation of the behavior of the model. For example, a trace (a set of desirable states and transitions) created on the abstract model may not replay on the concrete model. Its manual recreation, usually via animation, is necessary to run the trace, as the model may have changed significantly during refinement. However, this is a labor-intensive and error-prone task. To this end, this article presents an automatic trace refining technique and tool called BERT (B and Event-B Trace Refinement Technique) that allows modelers to ensure the behavioral integrity of high-level traces at the concrete level. The cost- and time-effectiveness of BERT are shown in industrial-strength case studies from the automotive and aviation domains.

This article presents a systematic mapping study on the model-driven engineering of safety and security concerns in software systems. Combined modeling and development of both safety and security concerns is an emerging field of research as both concerns affect one another in unique ways. Our mapping study provides an overview of the current state of the art in this field. This study carefully selected 143 publications out of 27,259 relevant papers through a rigorous and systematic process. This study then proposes and answers questions such as frequently used methods and tools and development stages where these concerns are typically investigated in application domains. Additionally, we identify the community's preference for publication venues and trends. The discussion on obtained results also features the gained insights and future research directions.