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.

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.

Context: Graphical user interface (GUI) testing of mobile applications (apps) is significant from a user perspective to ensure that the apps are visually appealing and user‐friendly. Pattern‐based GUI testing (PBGT) is an innovative model‐based testing (MBT) approach designed to enhance user satisfaction and reusability while minimizing the effort required to model and test UIs of mobile apps. In the literature, several primary studies have been conducted in the domain of PBGT. Problem: The current state‐of‐the‐art lacks comprehensive secondary studies within the PBGT domain. To our knowledge, this area has insufficient focus on in‐depth research. Consequently, numerous challenges and limitations persist in the existing literature. Objective: This study aims to fill the gaps mentioned above in the existing body of knowledge. We highlight popular research topics and analyze their relationships. We explore current state‐of‐the‐art approaches and techniques, a taxonomy of tools and modeling languages, a list of reported UI test patterns (UITPs), and a taxonomy of writing UITPs. We also highlight practical challenges, limitations, and gaps in the targeted research area. Furthermore, the current study intends to highlight future research directions in this domain. Method: We conducted a systematic literature review (SLR) on PBGT in the context of Android and web apps. A hybrid methodology that combines the Kitchenham and PRISMA guidelines is adopted to achieve the targeted research objectives (ROs). We perform a keyword‐based search on well‐known databases and select 30 (out of 557) studies. Results: The current study identifies 11 tools used in PBGT and devises a taxonomy to categorize these tools. A taxonomy for writing UITPs has also been developed. In addition, we outline the limitations of the targeted research domain and future directions. Conclusion: This study benefits the community and readers by better understanding the targeted research area. A comprehensive knowledge of existing tools, techniques, and methodologies is helpful for practitioners. Moreover, the identified limitations, gaps, emerging trends, and future research directions will benefit researchers who intend to work further in future research.

With AI increasingly affecting software systems, there is a pressing need to prepare the next generation of software engineers to build AI-intensive systems proficiently. This work outlines our instructional approach in the “Engineering of AI-intensive Systems” course for postgraduate computer science students to bridge the knowledge gap between software engi-neering (SE) and artificial intelligence (AI) disciplines. Our paper elaborates on the course's framework, pedagogical strategies, and evaluation methods, emphasizing the benefits of this interdisci-plinary educational model.

Refining high-level requirements into low-level ones is a common task, especially in safety-critical systems engineering. The objective is to describe every important aspect of the high-level requirement in a low-level requirement, ensuring a complete and correct implementation of the system's features. To this end, standards and regulations for safety-critical systems require reviewing the coverage of high-level requirements by all its low-level requirements to ensure no missing aspects.

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.

Summary In software development, developer turnover is among the primary reasons for project failures, leading to a great void of knowledge and strain for newcomers. Unfortunately, no established methods exist to measure how the problem domain knowledge is distributed among developers. Awareness of how this knowledge evolves and is owned by key developers in a project helps stakeholders reduce risks caused by turnover. To this end, this paper introduces a novel, realistic representation of problem domain knowledge distribution: the ConceptRealm. To construct the ConceptRealm, we employ a latent Dirichlet allocation model to represent textual features obtained from 300 K issues and 1.3 M comments from 518 open‐source projects. We analyze whether the newly emerged issues and developers share similar concepts or how aligned the individual developers' concepts are with the team over time. We also investigate the impact of leaving developers on the frequency of concepts. Finally, we also evaluate the soundness of our approach on a closed‐source software project, thus allowing the validation of the results from a practical standpoint. We find out that the ConceptRealm can represent the problem domain knowledge within a project and can be utilized to predict the alignment of developers with issues. We also observe that projects exhibit many keepers independent of project maturity and that abruptly leaving keepers correlates with a decline of their core concepts as the remaining developers cannot quickly familiarize themselves with those concepts.

Abstract Learning classifiers with uneven class distribution datasets poses a significant challenge in software defect prediction. This problem arises when the number of samples representing one class is significantly smaller than the others, leading to weak classification performance, particularly for minority class instances. Traditional classification models assuming equal class instances can result in low prediction accuracy and decision-making precision for minority class instances, raising concerns about identifying such instances accurately. To overcome this issue, this research proposes a hybrid technique that combines the Adaptive Synthetic Sampling (ADASYN) approach with a batch generator named the HADAB technique. ADASYN generates synthetic samples for the minority class, balancing the dataset and improving prediction accuracy. Conversely, the batch generator feeds data to the model in batches, enhancing training efficiency. The Multi-Layer Perceptron (MLP) serves as the base classifier in this study. The proposed HADAB technique significantly improves prediction accuracy and training efficiency without requiring additional parameter tuning, algorithm modification, or increasing complexity. We validate the performance of HADAB using publicly available NASA datasets encompassing diverse types. The results demonstrate the superiority of HADAB over traditional prediction accuracy methods. In conclusion, the proposed HADAB technique offers a practical and effective solution for handling class imbalance in software defect prediction, leading to improved prediction accuracy.

Abstract The quality of a pull request is the primary factor integrators consider for its acceptance or rejection. Code smells indicate sub‐optimal design or implementation choices in the source code that often lead to a fault‐prone outcome, threatening the quality of pull requests. This study explores code smells in 21k pull requests from 25 popular Java projects. We find that both accepted (37%) and rejected (44%) pull requests have code smells, affected mainly by god classes and long methods. Besides, we observe that smelly pull requests are more complex and challenging to understand as they have significantly large sizes, long latency times, more discussion and review comments, and are submitted by contributors with less experience. Our results show that features used in previous studies for pull request acceptance prediction could be potentially employed to predict smell in incoming pull requests. We propose a dynamic approach to predict the presence of such code smells in the newly added pull requests. We evaluate our approach on a dataset of 25 Java projects extracted from GitHub. We further conduct a benchmark study to compare the performance of eight machine learning classifiers. Results of the benchmark study show that XGBoost is the best‐performing classifier for smell prediction.

Cyber-physical systems (CPSs) interact with their physical environment by both monitoring and manipulating objects and processes from the real world. The range of applications for CPSs encompasses agriculture, aeronautics, energy, healthcare, manufacturing, robotics, and transportation, to name just a few. Often, CPSs are part of what we consider critical infrastructure, for example, electric power and water treatment. CPSs communicating with the outside world are security-critical. They open an attack vector through their communication channels. CPSs are safety-critical if they potentially harm their environment. Conventional protection mechanisms like secure design principles are insufficient. We need to guarantee our CPSs' resilience (cf. Segovia et al.1), that is, the ability of a system to withstand adverse events while maintaining an acceptable functionality.2 Communication and coordination features of CPSs demand a combined approach to consider both safety and security concerns. We have published several special issues on the topic of the safety and security of CPSs in previous years.3-6 Similarly, for the current special issue, a general call for articles was announced and also the authors of the best papers of the International Workshop on Cyber-Security and Functional Safety in Cyber-Physical Systems—IWCFS 20207 and IWCFS 20218 —were invited to submit extended versions of their workshop papers. After thorough and stringent reviews, we selected ten articles that provide relevant contributions to the field of safety and security for CPSs. In the article, Identifying Safety Issues from Energy Conservation Requirements by Madala by Do and Tenbergen, the authors propose an approach for identifying safety issues caused by energy conservation recommendations of CPSs. The authors then empirically study four robotic systems to evaluate the approach's effectiveness. The authors find that the energy conservation recommendations compromise safety at the concept phase. In the article, Context Modeling for Cyber-Physical Systems by Daun and Tenbergen, the authors propose a comprehensive, ontologically grounded context modeling framework to systematically explore the problem space in which a CPS under development will operate. This allows for the systematic elicitation of requirements for the CPS, early validation and verification of its properties, and safety assessment of its context interactions at runtime. In the article, Enhancing and Securing Cyber-physical Systems and Industry 4.0 through Digital Twins: A Critical Review by Lampropoulos and Siakas, the authors present an overview regarding the use of digital twins as a means to reinforce and secure CPSs and Industry 4.0 in general. The authors argue that based on the provided literature review, digital twins can constitute an essential tool for the realization, reinforcement, and security of CPSs and Industry 4.0. In the article, F3FLUID: A Formal Framework for Developing Safety-Critical Interactive Systems in FLUID by Singh, Ait-Ameur, Mendil, Méry, Navarre, Palanque, and Pantel, the authors propose a unified formal framework, F3FLUID (Formal Framework For FLUID), for the development of safety-critical interactive systems. This framework is based on the FLUID (Formal Language of User Interface Design) pivot modeling language that enables the specification of high-level system requirements for interactive systems. This modeling language is designed to handle safety-critical interactive systems concepts, including domain knowledge. An industrial case study complying with the ARINC 661 standard for avionics systems is used to illustrate the effectiveness of the F3FLUID framework for the development of safety-critical interactive systems. In the article, Modeling and Verifying NLSR Protocol of NDN for CPS Using UPPAAL by Fei, Zhu, and Yin, the authors attempt to formally model and verify some fundamental properties of the NLSR protocol using model checker UPPAAL. First, the authors validate the NLSR protocol modeled into timed automata with a simulator in UPPAAL. Then, they verify the model with four fundamental properties (termination, reachability of Sync Interest, reachability of Sync Data, and digest synchronization). The first synchronization problem is found in a scenario with two node topology. The authors then give the improved model, which owns a valid result in digest synchronization verification. To capture more problems, the authors make the model to support the simulation of a temporary network crash. The second synchronization problem is also exposed in two comparative scenarios. Finally, the authors also propose a mechanism implemented in the model, which validates digest synchronization verification results. In the article, An Automated Evaluation of MQTT Broker Compatibility by Sochor, Ferrarotti, and Ramler, the authors develop an automated framework for compatibility evaluation of Message Queuing Telemetry Transport (MQTT) brokers, which can be easily generalized to other similar IoT components. They apply this framework to perform a comprehensive experiment conducted with 16 different versions of six popular MQTT brokers. In this work, the authors report inconsistencies in the behavior of varying MQTT brokers and broker versions. Based on the experiment results, the authors calculate and provide a visualization of compatibility among the evaluated brokers regarding their distance, indicating the risk of incompatibilities when replacing a broker with another. The calculation of distance measures can be adjusted by giving higher weights to essential features. The authors use this method to show security-related differences between the brokers. In the article, Safety And Security Risks Management Process for Cyber-Physical Systems: A Case Study by Inayat, Farooq, and Inayat, the authors present an integrated safety-security risk management process. To demonstrate the efficacy of the proposed process, they used a tetra packaging case study to (i) examine the vulnerabilities of CPS by running the risk management process, (ii) identify safety-security requirements, and (iii) align retrieved safety-security requirements with the relevant standards. The results show (i) safety hazards and security risks along with their severity and priority, (ii) mitigation guidelines in accordance with IEC 61508, and (iii) 15 safety-security requirements that were identified and are aligned with ISO 9001 packaging and labeling machine standard. In the article, Uncertainty Handling in Cyber-Physical Systems: State-of-the-Art Approaches, Tools, Causes, and Future Directions by Asmat, Khan, and Hussain, the authors identify current state-of-the-art approaches, tools, root causes, and metrics for uncertainty in the domain of CPSs. In addition, they performed a systematic literature review. The core contributions of this study are: (i) to categorize the tools used for uncertainty mitigation and existing root causes of uncertainty in the CPSs domain, (ii) to categorize the tools used for uncertainty mitigation and existing root causes of uncertainty in the CPSs domain, and (iii) to identify the state-of-the-art methods which cannot elaborate the metrics to measure the uncertainty in CPSs. The results of the proposed study are beneficial in guiding future research on devising new approaches or tools to mitigate the causes of uncertainty in CPSs. In the article, Internet-of-Things Architectures for Secure Cyber-Physical Spaces: the VISOR Experience Report by Pascale, Cascavilla, Sangiovanni, Tamburri, and Heuvel, the authors conduct a field study in a Dutch Easter music festival in a national interest project called VISOR to select the most appropriate device configuration in terms of performance and results. They iteratively architect solutions for the security of cyber-physical spaces using IoT devices. They test the performance of multiple federated devices encompassing drones, closed-circuit television, smartphone cameras, and smart glasses to detect real-case scenarios of potentially malicious activities such as mosh-pits and pick-pocketing. The results pave the way to select optimal IoT architecture configurations, that is, a mix of CCTV, drones, smart glasses, and camera phones, to make safer cyber-physical spaces a reality. Finally, in the article, Model-Driven Engineering of Safety and Security Software Systems: A Systematic Mapping Study and Future Research Directions by Mashkoor, Egyed, Wille, and Stock, the authors present a systematic mapping study on the model-driven engineering of safety and security concerns in software systems. Combined modeling and development of safety and security concerns is an emerging field of research. The 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, the authors identify the community's preference for publication venues and trends. The discussion on obtained results also features the gained insights and future research directions. The editors of this special issue would like to thank the production team of Wiley for supporting the creation of this special issue. Special mention is also due to our reviewers, who processed all our submissions. Many thanks! This work is partially supported by the Austrian Science Fund (FWF) (grant # I 4744-N) and the LIT Secure and Correct Systems Lab funded by the State of Upper Austria.

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.

Abstract Engineering projects involve a variety of artifacts such as requirements, design, or source code. These artifacts, many of which tend to be interdependent, are often manipulated concurrently. To keep artifacts consistent, engineers must continuously consider their work in relation to the work of multiple other engineers. Traditional consistency checking approaches reason efficiently over artifact changes and their consistency implications. However, they do so solely within the boundaries of specific tools and their specific artifacts (e.g., consistency checking between different UML models). This makes it difficult to examine the consistency between different types of artifacts (e.g., consistency checking between UML models and the source code). Global consistency checking can help addressing this problem. However, it usually requires a disruptive and time-consuming merging process for artifacts. This article presents a novel, cloud-based approach to global consistency checking in a multi-developer/-tool engineering environment. It allows for global consistency checking across all artifacts that engineers work on concurrently. Moreover, it reasons over artifact changes immediately after the change happened, while keeping the (memory/CPU) cost of consistency checking minimal. The feasibility and scalability of our approach were demonstrated by a prototype implementation and through an empirical validation.

Requirement-to-code traces reveal the code location(s) where a requirement is implemented. Traceability is essential for code evolution and understanding. However, creating and maintaining requirement-to-code traces is a tedious and costly process. In this paper, we introduce TraceRefiner, a novel technique for automatically refining coarse-grained requirement-to-class traces to fine-grained requirement-to-method traces. The inputs of TraceRefiner are (1) the set of requirement-to-class traces, which are easier to create as there are far fewer traces to capture, and (2) information about the code structure (i.e., method calls). The output of TraceRefiner is the set of requirement-to-method traces (providing additional, fine-grained information to the developer). We demonstrate the quality of TraceRefiner on four case study systems (7-72KLOC) and evaluated it on over 230,000 requirement-to-method predictions. The evaluation demonstrates TraceRefiner's ability to refine traces even if many requirement-to-class traces are undefined (incomplete input). The obtained results show that the proposed technique is fully automated, tool-supported, and scalable.

This paper proposes a recommendation approach for issues (e.g., a story, a bug, or a task) prioritization based on natural language processing, called NLP4IP. The proposed semi-automatic approach takes into account the priority and story points attributes of existing issues defined by the project stakeholders and devises a recommendation model capable of dynamically predicting the rank of newly added or modified issues. NLP4IP was evaluated on 19 projects from 6 repositories employing the JIRA issue tracking software with a total of 29,698 issues. A comprehensive benchmark study was also conducted to compare the performance of various machine learning models. The results of the study showed an average top@3 accuracy of 81% and a mean squared error of 2.2 when evaluated on the validation set. The applicability of the proposed approach is demonstrated in the form of a JIRA plug-in illustrating predictions made by the newly developed machine learning model. The dataset has also been made publicly available in order to support other researchers working in this domain.

Software engineers use requirement-to-method trace matrices to indicate the methods implementing different system requirements. Requirement-to-method trace matrices pinpoint the exact method implementing each requirement, which facilitates software maintenance and bug fixing. The code structure of a system can be used to make predictions about requirement-to-method traces. In this paper, we present a data set documenting the requirement-to-method traces as well as the code structure (methods, variables, etc.) for four open source systems. The code structure was obtained by parsing the systems under consideration and extracting the methods, variables, etc. The requirement-to-method trace matrices were obtained by resorting to students as well as to the original developers of the systems who provided us with the list of requirement-to-method traces.

Abstract Cyber‐Physical Systems (CPSs) differ from traditional Information Technology (IT) systems in such a way that they interact with the physical environment, i.e., they can monitor and manipulate real objects and processes. For this special issue, the authors of the best papers of IWCFS 2019 were invited to submit extended versions of their workshop papers. Additionally, we received eight submissions from around the globe as a result of an open call. After thorough and stringent reviews, we selected six articles that provide relevant contributions to the field of safety and security for CPSs.

Abstract In today's engineering projects, companies continuously have to adapt their systems to changing customers or dynamic market requirements. This requires a flexible, iterative development process in which different parts of the system under construction are built and updated concurrently. However, concurrent engineering becomes quite challenging in domains where different engineering artifacts from different disciplines come into play, such as safety‐critical cyber‐physical systems, where the involved engineering artifacts are quite heterogeneous in nature. In such systems, it is of utmost importance that different artifacts remain consistent in order to guarantee a correctly functioning end product. In this article, we discuss our experiences (with a leading company working in the areas of production automation and product processing) in maintaining the consistency between electrical models and the corresponding software controller, when both are subject to continuous changes. The article discusses how we let engineers describe the relationships between electrical models and the corresponding software controller code in the form of links and consistency rules. Additionally, we demonstrate that how our approach, through a process of continuous consistency checking, notifies engineers about the erroneous impact of their changes in various engineering artifacts.

The new era of Industry 4.0 is leading towards self-learning and adaptable production systems requiring efficient and intelligent decision making. Achieving high production rate in a short span of time, continuous improvement, and better utilization of resources is crucial for such systems. This paper discusses an approach to achieve production optimization by finding optimal sequences of orders, which yield high throughput using reinforcement learning. The feasibility of our approach is evaluated by simulating a plant modelled on a higher level of abstraction taken from a real assembly line. The applicability of the proposed approach is demonstrated in the form of code utilizing the simulation model. The obtained results show promising accuracy of sequences against corresponding throughput during the simulation process.

Abstract Contemporary interaction‐based complex systems are often built by reusing existing distributed peers, which have to coordinate with each other to fulfill the client, system, and environment requirements. In this paper, we address the design of distributed systems composed of peers (state‐transitions systems) communicating through message exchanges. We consider choreographies as the formal model, allowing a developer to describe and specify peers coordination as a set of conversations; ie, all sequences of messages exchanged between the communicating peers. Proceeding this way requires building neither the individual peers nor their composition as they may be obtained by the choreography projection. The correctness of the preservation of such messages exchanges by each peer obtained after projection is a key issue, known as the realizability problem. Checking choreography realizability is mandatory to build third‐party applications with no coordination error, eg, absence of deadlocks, missing messages, and erroneous messaging order. In our previous work, we have proposed a set of composition operators, allowing designers to build realizable choreographies that are represented by conversation protocols (CPs). In this work, realizability is guaranteed by construction. We rely on the correct‐by‐construction Event‐B method to prove that each CP constructed using our operators is realizable. In this paper, we show how our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. We also show that our approach allows to detect failures and failure recovery in case realizability does not hold.

Abstract According to best practices of model‐driven engineering, the implementation of a system should be obtained from its model through a systematic model‐to‐code transformation. We present in this paper a methodology supported by the Asm2C++ tool, which allows the users to generate C++ code from abstract state machine models. Thanks to Asm2C++, the implementation is generated in a seamless manner with an assurance of potential bug freeness of the generated code. Following the same approach, model‐based testing suggests deriving also (unit) tests from abstract models. We extend the Asm2C++ tool such that it can automatically produce unit tests for the generated code. Abstract test sequences, either generated randomly or through model checking, are translated to concrete C++ unit tests using the Boost library. In a similar manner, also, scenarios are generated in a behavior‐driven development (BDD) approach. To guarantee the correctness of the transformation process, we define a mechanism to test the correctness of the model‐to‐code transformation with respect to two main criteria: syntactical correctness and semantic correctness, which is based on the definition of conformance between the specification and the code. Using this approach, we have devised a process able to test the generated code by reusing unit tests. The process has been used to validate our model‐to‐code transformations.

Security-and safety-critical cyber-physical systemsCyber-physical systems (CPSs) are physical embedded systems with enhanced operations for monitoring, coordination, control, and integration by a computing and communication core. 1 Examples of CPSs include transportations systems, 2 medical systems, 3 and manufacturing systems.4 A CPS can be security-critical, safety-critical, or both.A CPS communicating with the outside world and thus opening an attack vector through the communication channel is considered to be a security-critical CPS.On the other hand, a CPS is considered to be safety-critical if it can harm its environment, eg, a malfunctioning autonomous vehicle might harm its passengers.5 A CPS dealing with both security and safety concerns is considered to be a security-and safety-critical CPS.Contemporary systems and software engineering methods often prove inadequate for the trustworthy and reliable design and engineering of CPSs.Traditional engineering deals with security and safety issues as separate problems.However, given the coordination and communication features of CPSs, such a ''separation-of-concerns'' approach is no longer adequate.We need integrated methods to deal with security and safety concerns within CPSs.

In this paper, we address the design of distributed systems composed of peers (state-transitions systems) communicating through message exchanges. We consider choreographies as the ground formal model allowing a developer to describe and specify peers coordination as a set of conversations, i.e., all sequences of messages exchanged between the communicating peers. Proceeding this way does not require building the individual peers, nor their composition; they may be obtained by choreography projection. The correctness of the preservation of such messages exchanges by each peer obtained after projection is a key issue, known as the realizability problem. In our previous work [1], we have proposed a set of composition operators allowing designers to build realizable choreographies that are represented by conversation protocols (CPs). We rely on the correct-by-construction Event-B method to prove that each CP constructed using our operators is realizable. In this paper, we show how our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. We also show that our approach allows to detect failures and failure recovery in case realizability does not hold

The use of software has become ubiquitous and prevalent in modern medical devices such as hemodialysis machines. Consequently, the failure rate of medical devices due to software faults is also increasing. While next-generation software-intensive medical devices contribute to providing better health care and ease of use, their development is becoming unprecedentedly complex and challenging. The critical nature of this domain - particularly its direct implications on health and safety - requires extraordinary measures to ensure the correct and reliable function of such systems. Formal methods are proven to provide approaches, techniques, and tools for correct engineering of software and systems. However, their use in the contemporary medical software engineering is still marginal. In order to promote the use of (state-based) formal methods and showcase their effectiveness in design and development of critical medical devices, we present the hemodialysis case study challenge problem in this article. We also analyze the novelties and limitations of several solutions implementing the case study and explore research challenges that still need to be addressed in future.

Abstract The use of formal methods is often recommended to guarantee the provision of necessary services and to assess the correctness of critical properties, such as functional safety, cybersecurity, and reliability, in medical and health care devices. In the past, several formal and rigorous methods have been proposed and consequently applied for trustworthy development of medical software and systems. In this paper, we perform a systematic literature review on the available state of the art in this domain. We collect the relevant literature on the use of formal methods for modeling, design, development, verification, and validation of software‐intensive medical systems. We apply standard systematic literature review techniques and run several queries in well‐known repositories to obtain information that can be useful for people who are either already working in this field or planning to start. Our study covers both quantitative and qualitative aspects of the subject.

Selected functional safety and cybersecurity concerns in system, software, and service process improvement and innovationIn this editorial, we present a set of papers related to the European System and Software Process Improvement and Innovation Initiative (EuroSPI 2 ) launched back in 1994.With more than 20 editions of the conference and around 20 special issues devoted to the initiative 1-13 with the majority of them published in the Journal of Software: Evolution and Process and its predecessors, the community has contributed vastly to the development of the discipline.This special issue presents papers sent as extended versions of previous papers published in the proceedings including also papers indirectly linked to the conference.The focus of this special issue is functional safety and cybersecurity as related to software and service improvement and innovation.Nowadays, nearly all organizations depend on appropriate secure and compliant information processing based on different software systems.14 As a consequence of this importance, the EuroSPI 2 community has approached the topic from a panoply of viewpoints including traceability aspects, 15 safety and availability improvement, 16 process assessment in safety, 17 and action research approaches in financial organizations, 18 naming just some of the more recent and relevant initiatives.This special issue enhances previous efforts by providing an updated and extended view on the implications of security aspects in the service and process improvement and innovation arena.The paper "Extending Automotive SPICE 3.0 for the Use in ADAS and Future Self-Driving Service Architectures" by Richard Messnarz, Christian Kreiner, Georg Macher, and Alastair Walker summarizes the current state of the art and extends the existing concepts of a service architecture supporting the car-to-car and car-to-cloud communication.This leads to an additional service life cycle model that can be plugged into Automotive SPICE (Software Process Improvement and Capability Determination) 3.01.The article also shows an example of a process that needs to be assessed as well to cover not only the vehicle but also the entire service architecture in an assessment and analysis.The paper "Software Quality Model for a Research-driven Organization-An Experience Report" by Marcin Wolski, Bartosz Walter, Szymon Kupiński, and Jakub Chojnacki presents a measurement framework for evaluating quality in software products developed within the research and innovation framework project GEANT2.The proposed framework is based on the quality models by Boehm 19 and McCall 20 but also presents

Summary After a number of success stories in safety‐critical domains, we are starting to witness applications of formal methods in contemporary systems and software engineering. However, one thing that is still missing is the evaluation criteria that help software practitioners choose the right formal method for the problem at hand. In this paper, we present the criteria for evaluating and comparing different formal methods. The criteria were chosen through a literature review, discussions with experts from academia and practitioners from industry, and decade‐long personal experience with the application of formal methods in industrial and academic projects. The criteria were then evaluated on several model‐oriented state‐based formal methods. Our research shows that besides technical grounds (eg, modeling capabilities and supported development phases), formal methods should also be evaluated from social and industrial perspectives. We also found out that it is not possible to generate a matrix that renders the selection of the right formal method an automatic process. However, we can generate several pointers, which make this selection process a lot less cumbersome.

Medical device software malfunctioning can lead to injuries or death for humans and, therefore, its development should adhere to certification standards. However, these standards establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability. This paper presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.

This paper explores the possibility to incorporate validation in the stepwise development process of formal specifications. Formal methods based on refinement break the intractable proof of the correctness of implementation into a sequence of many smaller proofs. Likewise, the validation of the specification could be broken into smaller steps associated to refinements with the technique of animation. Animating an abstract specification often requires to alter it in ways that proof obligations cannot be discharged anymore. So, we have developed a process and a set of transformation rules whose application produces an anima table specification which may be non-provable, but which is assured to have the same behavior. Guaranteeing behavioral preservation requires us to define an ad-hoc relationship between specifications based on a kind of trace semantics. 10 rules have been identified and proven to preserve behavior. Observations on the use of the technique on two case-studies are presented.

Well specified requirements are crucial for good software design and domain engineering helps better understanding and specification of requirements. Safety critical domains, such as transportation, exhibit interesting features, such as high levels of non-determinism, complex interactions, stringent safety properties, multifaceted timing attributes, etc. The formal representation of these features is a challenging task. This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. We explore the possibility of using Event-B as a domain engineering tool. We discuss the problems posed by the introduction of time and how we tackle it. We design a technique based on animation to validate domain models.

The main aim of this paper is to present how to derive logical software architectures for CRUD (Create, Read, Update and Delete) applications using a specific technique called 4SRS. In this technique, a component diagram, which is obtained through transformations of use cases, is used to represent the logical software architecture. To show that the 4SRS technique, which was initially devised for behavior-intensive reactive systems, is also effective and gives seamless results for other software domains, it is being experimented on data processing systems, which typically follow a CRUD pattern. For demonstration purposes, the FPL tower interface system, which is responsible for communication between air traffic control operators and flight data processing system on airports of Portugal, has been used as a case study.