The safety requirements are often described via specifications called contracts. To verify that the system fulfills certain safety requirements, for instance, in the assume-guarantee contract specification, the key safety indicators are organized, so that if certain assumptions hold then the respective behaviour is guaranteed. Safety contracts provide a means of exposing potential incompatibilities early in the development process, selecting components to reuse, certifying systems, and identifying uncertainty sources during the operational phase. There exist several studies on contract-based safety assurance, however, there is not any systematic study in this field. For this, a first Systematic Literature Review (SLR) is carried out to obtain an overview of the various contract-based safety assurance concepts, problems, proposed solutions, and their usefulness. In our study, the identification and selection of the primary studies were based on a well-planned search strategy. The search process identified a total of 2881 studies published between 1969 and 2021, out of which 66 studies were selected through a multi-stage process according to our predefined SLR protocol. This SLR aims to highlight the state-of-the-art of contract-based safety assurance and identify potential gaps for future research. Based on research topics in selected studies, we identified the following main categories: contract type, analysis techniques for system safety, compliance with standards, development stage, domain, level of automation, type of study and evaluation, and tool support. The findings of the systematic review not only highlight that the contracts are even more important for advanced safety-critical systems but also strategies to exploit their full potential should be considered in future studies. The suggestions revealed for future research include the usage of contracts for adapting new behaviour, defining system boundaries, interacting with other systems, managing risk during operation, dynamic/runtime safety assurance, and integration of safety with security.

Energy storage systems, especially lithium-ion batteries have gained significant attention and interest due to their potential in storing electrical energy and environmental sustainability. They play a crucial role in electric vehicles and significantly impact their performance, particularly in terms of electric driving range and quick acceleration. Despite their advantages, lithium-ion batteries also have limitations. These include the potential for thermal runaway, which can lead to safety hazards if not properly managed, such as outgassing, fire, and explosion that in turn cause significant property damage and fatalities. Published studies on road vehicles have not adequately considered the safety assurance of rechargeable energy storage systems in accordance with ISO 26262 standard. Accordingly in this paper, we focus on the safety assurance of a battery management system (BMS) that prevents thermal runaway and keeps lithium-ion batteries safe in electric vehicles. To this end, the safety life cycle process is performed. At first, the potential hazards that lead to thermal runaway impacting the functions of electric vehicles have been identified and safety goals related to means for preventing and controlling hazards are formulated. Next, the functional safety requirements are derived from each safety goal, and subsequently technical safety requirements are derived. To demonstrate the acceptable safety of electric vehicles using the BMS strategy, the safety cases are developed from the functional safety activities. The safety contracts are derived from battery specifications and chemistry and are associated with safety cases that provide the means for performing necessary adaptations at the operational phase. We leveraged a simulation for performing the verification and validation as well as finetuning of the BMS strategy. Simulation data is gathered, and the critical parameters are monitored to determine safety violations, control actions are triggered to resolve them, and safety cases are updated to reflect the current system safety.

The assurance case arguments are created to demonstrate acceptable system safety and/or security. In this regard, a series of propositions expressed by natural language statements (claims) are broken down into sub-claims representing a logical chain of reasoning until the corresponding evidence is obtained. The review and update of assurance arguments for aligning with the process and product counterparts used for their construction are essential tasks. These tasks are perceived as challenging but can be efficiently supported by using Natural Language Processing (NLP). To date, however, the published studies on assurance cases have not leveraged the NLP. Accordingly, this paper presents our NLP-based assurance framework called ATTEST. At first, the text preprocessing is carried out by using NLP tasks. The rules are created, in which both syntactic and semantic features are captured. The former is captured by using NLP tasks, while the latter is captured by the internal structure of models as well as the mappings across them. The created rules are triggered for argument comprehension, well-formedness, sufficiency checks, and identifying defeaters and counter-evidence selection. Besides the process, product, and assurance case models produced during the design and development phase, the operational data is gathered from the configured simulation environments and used for identifying problems as well as the measures for resolving them. Finally, the affected parts of assurance case models are highlighted and the underlying reasoning for their adaptation is presented. The applicability of the proposed framework is demonstrated by reviewing and updating assurance cases constructed for vehicular Accelerator Control System (ACS) with Electronic Throttle Control (ETC).

Abstract The processes used to develop software need to comply with normative requirements (e.g., standards and regulations) to align with the market and the law. Manual compliance checking is challenging because there are numerous requirements with changing nature and different purposes. Despite the importance of automated techniques, there is not any systematic study in this field. This lack may hinder organizations from moving toward automated compliance checking practices. In this paper, we characterize the methods for automatic compliance checking of software processes, including used techniques, potential impacts, and challenges. For this, we undertake a systematic literature review (SLR) of studies reporting methods in this field. As a result, we identify solutions that use different techniques (e.g., anthologies and metamodels) to represent processes and their artifacts (e.g., tasks and roles). Various languages, which have diverse capabilities for managing competing and changing norms, and agile strategies, are also used to represent normative requirements. Most solutions require tool‐support concretization and enhanced capabilities to handle processes and normative diversity. Our findings outline compelling areas for future research. In particular, there is a need to select suitable languages for consolidating a generic and normative‐agnostic solution, increase automation levels, tool support, and boost the application in practice by improving usability aspects.

The capability to dynamically reconfigure in response to change of mode or function, failures, or unanticipatedhazardous conditions is fundamental for many critical systems. The modelling and verification of suchsystems are frequently carried out with product lines and model checking, respectively. At first, the objectivesand related requirements of reconfigurable systems are mapped to a feature model, whereas the units relatedto operational modes are selected in individual configurations. After that, the proposed approach performsautomated transformation of particular models into formal constraints and descriptions for leveraging the analyticalpowers of model checking techniques; the formal verification of completeness, consistency and conflictis carried out with NuSMV model checker. Finally, in circumstances when the counterexample is produced, itsanalysis is performed for the identification of corresponding problems and their resolutions. The applicabilityof the proposed approach is demonstrated through case study of attitude and orbit control system.

The drones provide an active measure to identify, monitor, analyze and resolve risks of autonomous systems during operational phase. To date, however, the published studies have not considered them for managing risks in a dynamic manner. The capability to deal with unknowns and uncertainties during operational phase is regarded as essential to exploit the autonomous systems at their full potential. This paper targets the drone-based assurance of autonomous systems. The hazard and threat analyses are performed during design and development phase by using the Hazard and Operability (HAZOP) and Threat and Operability (THROP) techniques, respectively. Based on the analyses results, the safety and security requirements are derived. The assume-guarantee contracts are also derived for uncertainty sources; they are integrated in the blockchain-based smart contracts. The simulators are leveraged for performing the verification and validation as well as improving systems. For assuring safety and security during operational phase, the contracts derived for uncertainty sources are checked. In case of divergence, the drones provide assistance; otherwise, depending on the severity risk factor, system control is taken to avoid the mishap risk. The applicability of the proposed methodology is exemplified in the context of a quarry site production scenario.

The goal of Industry 4.0 is to be faster, more efficient and more customer-centric, by enhancing the automation and digitalisation of production systems. Frequently, the production in Industry 4.0 is categorised as safety-critical, for example, due to the interactions between autonomous machines and hazardous substances that can result in human injury or death, damage to machines, property or the environment. In order to demonstrate the acceptable safety of production operations, safety cases are constructed to provide comprehensive, logical and defensible justification of the safety of a production system for a given application in a predefined operating environment. However, the construction and maintenance of safety cases in alignment with Industry 4.0 are challenging tasks. For their construction, besides the modular, dynamic and reconfigurable nature of Industry 4.0, the architectural levels of the things, fog and cloud computing have to be considered. The safety cases constructed at system design and development phases might be invalidated during production operations, thus necessitating some means for dynamic safety assurance. Moreover, flexible manufacturing in Industry 4.0 also underlines the need for safety assurance in a dynamic manner during the operational phase. Currently published studies are not explicitly supporting the safety assurance of Industry 4.0, which is the focus of this paper with special emphasis on dynamic safety assurance. At first, the Hazard and Operability (HAZOP) and Fault Tree Analysis (FTA) techniques are used for the identification and mitigation/elimination of potential hazards. Next, based on the hazard analysis results, we derived the safety requirements and safety contracts. Subsequently, safety cases are constructed using the OpenCert platform and safety contracts are associated with them to enable necessary changes during runtime. Finally, we use a simulations based approach to identify and resolve the deviations between the system understanding reflected in the safety cases and the current system operation. The dynamic safety assurance is demonstrated using a use case scenario of materials transportation and data flow in the Industry 4.0 context.

Automated Guided Vehicles (AGVs) are widely used for materials transportation. Operating them in a platooned manner has the potential to improve safety, security and efficiency, control overall traffic flow and reduce resource usage. However, the published studies on platooning focus mainly on the design of technical solutions in the context of automotive domain. In this paper we focus on a largely unexplored theme of platooning in production sites transformed to the Industry 4.0, with the aim of providing safety and security assurances. We present an overall approach for a fault- and threat tolerant platooning for materials transportation in production environments. Our functional use cases include the platoon control for collision avoidance, data acquisition and processing by considering range, and connectivity with fog and cloud levels. To perform the safety and security analyses, the Hazard and Operability (HAZOP) and Threat and Operability (THROP) techniques are used. Based on the results obtained from them, the safety and security requirements are derived for the identification and prevention/mitigation of potential platooning hazards, threats and vulnerabilities. The assurance cases are constructed to show the acceptable safety and security of materials transportation using AGV platooning. We leveraged a simulation-based digital twin for performing the verification and validation as well as finetuning of the platooning strategy. Simulation data is gathered from digital twin to monitor platoon operations, identify unexpected or incorrect behaviour, evaluate the potential implications, trigger control actions to resolve them, and continuously update assurance cases. The applicability of the AGV platooning is demonstrated in the context of a quarry site.

The current trends of digitalization and Industry 4.0 are bringing ample opportunities for manufacturing industry to fine tune their products and processes at will, to meet changing market needs within short notice. However, the characteristics of advanced production systems, such as dynamic interactions between machines and reconfigurations, if not carefully orchestrated, could potentially lead to production failures or mishaps, making them safety-critical. Previous studies on hazard analysis, safety-performance tradeoffs and assurance cases have not specifically considered the dynamic reconfiguration scenarios in production systems. In this paper, for the hazard identification and mitigation/elimination, the principal characteristics of highly reconfigurable production systems have been given special consideration. Even if the hazard analysis results are incorporated in the initial designs of production systems, operational changes, such as adding/removing machines in response to market demands, system failures, or unanticipated hazardous conditions may still adversely impact the production safety and operational performance. For the operational changes, we perform the quantitative assessment through configuration analytics to determine the corresponding impacts on safety, performance and production demands. After that, the assurance case models are obtained with production line to cope with the potential problems during the dynamic safety assurance. The applicability of the proposed methodology is demonstrated in the context of a quarry site production scenario.

Compliance with process-based safety standards may imply the provision of a safety plan and its corresponding compliance justification. However, the provision of this justification is time-consuming since it requires that the process engineer checks the fulfillment of hundred of requirements by taking into account the evidence presented in the process entities. In this paper, we aim at supporting process engineers by introducing our compliance checking vision, which consists of the combination of process modeling capabilities via SPEM 2.0 (Systems & Software Process Engineering Metamodel) reference implementations and compliance checking capabilities via Regorous, a compliance checker, used for business processes compliance checking. Our focus is on the identification and exploitation of the appropriate (minimal set of) SPEM 2.0-like elements, available in the selected reference implementation, which can be used by Regorous for compliance checking. Then, we illustrate our vision by applying it onto a small excerpt from ISO 26262. Finally, we draw our conclusions.

The main challenge in software development process is to detect and fix the deviations of system's behaviors at different abstraction levels in early phases. For this purpose, UML 2 sequence diagrams are widely used for describing and analyzing the communication behavior of software systems. This paper describes a containment checking approach for UML 2 sequence diagrams to verify whether the behavior (or functions) described by a low-level model conforms those specified in the high-level counterpart based on model checking techniques, in order to improve the system's quality. However, creating consistency constraints and formal specifications for the sequence diagrams is a labor-intensive and error prone task. To alleviate this issue, we propose an automated transformation of sequence diagrams into formal specifications and consistency constraints that enable us to leverage the analytical powers of model checking to automatically verify the containment relationship. In addition, our approach provides the stakeholders more informative and comprehensive feedbacks regarding the inconsistency issues, and therefore helps them to efficiently identify and resolve the problems. The approach is implemented and validated using three realistic scenarios.

In the development of complex and large scale software systems, it is important to detect and fix the deviations of systems' behaviors at different abstraction levels in early phases. Our main focus here is the containment checking -- a special type of consistency checking -- that verifies whether the behavior (or functions) described by a low-level behavior model encompasses those specified in the high-level counterpart. As shown in our previous work, containment checking can be realized based on model checking, but not always the costly exhaustive searches employed by model checking are necessary for addressing the containment checking problem, leading to potentials for optimization. In addition, model checking and similar techniques often yield the checking results as true (satisfied) or false (unsatisfied) with error traces (e.g., Counter-examples). Unfortunately, such feedback is rather not helpful for users with limited background on the underlying formal methods to analyze and understand the causes of consistency violations. In this paper, we propose a lightweight graph-based approach for addressing the aforementioned problems of containment checking. The theoretical complexity of our approach is a cubic polynomial of the number of elements of the input behavior models. Additionally, we aim at generating feedbacks that are relevant and easy-to-understand for the stakeholders. Our approach is illustrated and evaluated on UML activity diagrams -- that are widely used for modeling behaviors of software systems -- using use cases derived from industrial scenarios.