Tim Kelly

Erik Armengaud, Georg Macher, Alexander Massoner et al.

The open and cooperative nature of Cyber-Physical Systems (CPS) poses new challenges in assuring dependability. The DEIS project (Dependability Engineering Innovation for automotive CPS. This project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No 732242, see http://www.deis-project.eu) addresses these challenges by developing technologies that form a science of dependable system integration. In the core of these technologies lies the concept of a Digital Dependability Identity (DDI) of a component or system. DDIs are modular, composable, and executable in the field facilitating (a) efficient synthesis of component and system dependability information over the supply chain and (b) effective evaluation of this information in-the-field for safe and secure composition of highly distributed and autonomous CPS. The paper outlines the DDI concept and opportunities for application in four industrial use cases.

Nikita Johnson, Youcef Gheraibia, Tim Kelly

Safety Security Assurance Framework applied to two standards IEC 61508 and Common Criteria - ISO 15408

Simon Foster, Yakoub Nemouchi, Mario Gleirscher et al.

Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.

Yakoub Nemouchi, Simon Foster, Mario Gleirscher et al.

Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty reasoning, and inadequate evidentiary support. However, assurance cases can rarely be fully formalised, as the use of formal methods is contingent on models validated by informal processes. Consequently, we need assurance techniques that support both formal and informal artifacts, with explicated inferential links and assumptions that can be checked by evaluation. Our contribution is a mechanical framework for developing assurance cases with integrated formal methods based in the Isabelle system. We demonstrate an embedding of the Structured Assurance Case Meta-model (SACM) using Isabelle/DOF, and show how this can be linked to formal analysis techniques originating from our verification framework, Isabelle/UTP. We validate our approach by mechanising a fragment of the Tokeneer security case, with evidence supplied by formal verification.

Nikita Johnson, Tim Kelly

Integrated safety and security assurance for complex systems is difficult for many technical and socio-technical reasons such as mismatched processes, inadequate information, differing use of language and philosophies, etc.. Many co-assurance techniques rely on disregarding some of these challenges in order to present a unified methodology. Even with this simplification, no methodology has been widely adopted primarily because this approach is unrealistic when met with the complexity of real-world system development. This paper presents an alternate approach by providing a Safety-Security Assurance Framework (SSAF) based on a core set of assurance principles. This is done so that safety and security can be co-assured independently, as opposed to unified co-assurance which has been shown to have significant drawbacks. This also allows for separate processes and expertise from practitioners in each domain. With this structure, the focus is shifted from simplified unification to integration through exchanging the correct information at the right time using synchronisation activities.

Chris Leong, Tim Kelly, Rob Alexander

In system development, epistemic uncertainty is an ever-present possibility when reasoning about the causal factors during hazard analysis. Such uncertainty is common when complicated systems interact with one another, and it is dangerous because it impairs hazard analysis and thus increases the chance of overlooking unsafe situations. Uncertainty around causation thus needs to be managed well. Unfortunately, existing hazard analysis techniques tend to ignore unknown uncertainties, and system stakeholders rarely track known uncertainties well through the system lifecycle. In this paper, we outline an approach to managing epistemic uncertainty in existing hazard analysis techniques by focusing on known and unknown uncertainty. We have created a reference populated with a wide range of safety-critical causal relationships to recognise unknown uncertainty, and we have developed a model to systematically capture and track known uncertainty around such factors. We have also defined a process for using the reference and model to assess possible causal factors that are suspected during hazard analysis. To assess the applicability of our approach, we have analysed the widely-used MoDAF architectural model and determined that there is potential for our approach to identify additional causal factors that are not apparent from individual MoDAF views. We have also reviewed an existing safety assessment example (the ARP4761 Aircraft System analysis) and determined that our approach could indeed be incorporated into that process. We have also integrated our approach into the STPA hazard analysis technique to demonstrate its feasibility to incorporate into existing techniques. It is therefore plausible that our approach can increase safety assurance provided by hazard analysis in the face of epistemic uncertainty.

Radu Calinescu, Danny Weyns, Simos Gerasimou et al.

Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.