Assurance cases are used to communicate and assess confidence in critical system properties such as safety and security. Historically, assurance cases have been manually created documents, which are evaluated by system stakeholders through lengthy and complicated processes. In recent years, model-based system assurance approaches have gained popularity to improve the efficiency and quality of system assurance activities. This becomes increasingly important, as systems becomes more complex, it is a challenge to manage their development life-cycles, including coordination of development, verification and validation activities, and change impact analysis in inter-connected system assurance artifacts. Moreover, there is a need for assurance cases that support evolution during the operational life of the system, to enable continuous assurance in the face of an uncertain environment, as Robotics and Autonomous Systems (RAS) are adopted into society. In this paper, we contribute ACCESS - Assurance Case Centric Engineering of Safety-critical Systems, an engineering methodology, together with its tool support, for the development of safety critical systems around evolving model-based assurance cases. We show how model-based system assurance cases can trace to heterogeneous engineering artifacts (e.g. system architectural models, system safety analysis, system behaviour models, etc.), and how formal methods can be integrated during the development process. We demonstrate how assurance cases can be automatically evaluated both at development and runtime. We apply our approach to a case study based on an Autonomous Underwater Vehicle (AUV).

Abstract Many tools can check if a test set provides control coverage; they are, however, of little or no help when coverage is not achieved and the test set needs to be completed. In this paper, we describe how a formal characterisation of a coverage criterion can be used to generate test data; we present a procedure based on traditional programming techniques like normalisation, and weakest precondition calculation. It is a basis for automation using an algebraic theorem prover. In the worst situation, if automation fails to produce a specific test, we are left with a specification of the compliant test sets. Many approaches to model-based testing rely on formal models of a system under test. Our work, on the other hand, is not concerned with the use of abstract models for testing, but with coverage based on the text of programs.

Abstract Control engineers make extensive use of diagrammatic notations; control law diagrams are used in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful, but verification of their implementations is a challenge that has been taken up by few. We are aware only of approaches that rely on automatic code generation, which is not enough assurance for certification, and often not adequate when tailored hardware components are used. Our work is based onCircus, a notation that combines Z, CSP, and a refinement calculus, and on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams. We present a strategy to translate Simulink diagrams toCircus, and a strategy to prove that a parallel Ada implementation refines theCircusspecification; we rely on aCircussemantics for the program. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of a large set of diagrams, and support verification of a large number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling.

Assurance of software systems has traditionally been sought through the rigour of the development process. The higher the assurance, the more demanding the development process; the highest assurance requiring the use of formal methods during development. This approach has been followed for decades with some success, but increased assurance brings a disproportionate increase in cost and risk. A change in emphasis is suggested from the development of a system to its acceptance. The benefits for high assurance systems are illustrated through a case study and preliminary experience of high assurance techniques are reported.

ClawZ is a prototype tool whose objective is to link the Simulink(R) control engineering tool from MathWorks, with the ProofPower(R) dialect of Z. It provides a bridge between the use of Simulink to define control law diagrams and a tool to formally prove compliance between Ada and Z. The tool has been used as part of the formal proof of a nonlinear dynamic inversion flight control system comprising 37 pages of diagrams, 45 pages of Z and 1200 lines of non-comment Ada.

This paper presents the advantages and disadvantages of automatic code generation of safety critical software. It discusses three broad approaches to its generation in the context of the high levels of assurance required. Finally a number of issues that commercial tool vendors must address are discussed along with consequent research issues that follow.

Any system constructed today is likely to be constructed from COTS components. Encapsulation of these components using software wrappers promises to enable trusted systems to be constructed. These systems are complex and it is difficult to impose security without compromising operational effectiveness. The key problem which this paper addresses is to analyse encapsulations of COTS components to demonstrate the system is both secure and usable. Any foundation must be able to deal with the conflicting requirements of operational effectiveness and security especially with respect to COTS components. The approach is illustrated using the X windowing system.

Tools such as Simulink(R) are being used by engineers around the world to model and solve real problems about dynamical systems. In particular control systems are modelled graphically, simulated and then code is generated automatically. Code generated from such a tool is being proposed for use in safety critical control systems. The problem for certifiers is why should they trust such generated code? This paper describes a particular approach to solving this problem which supports review by a certifier. A small case study is presented to illustrate the approach and the technical issues involved.

Describes a notation and tool for demonstrating to a third-party certifier that software written in a subset of Ada is safe, and gives some experience of using them on real projects. The thesis underlying the design is that people write adequate code, but that they make design and implementation decisions which can conflict with each other to introduce safety problems. The usual paradigm of formally specifying and then developing and verifying the code is less cost-effective than writing the code and then abstracting it to a level that is suitable for human judgements to be made. This is because there are more people who know how to write good code than those who can write effective formal specifications. The tool processes a formal, or informal, argument that code meets its safety requirements using literate programming and concepts from the refinement calculus developed at Oxford University.

Abstract A commonly made criticism of formal methods is that they increase costs. Selective use of formal methods to define critical requirements can, however, lead to a significant decrease in lifecycle costs. In particular the economic and technical benefits of outsourcing the development of software can be fully realized and the cost of outsourcing slightly reduced by use of a formal specification. In this paper we describe a development in which a formal specification prepared by the customer formed part of the contract with the supplier. We conclude that this use of a formal specification can reduce risks and costs for all concerned and can help foster fruitful and co-operative relations in situations which are often fraught with confrontation.

Any foundation for computer security needs to be tested to see whether it is strong enough to support a useful theory. In this paper a case study is presented which illustrates a particular foundation for confidentiality. A natural language confidentiality requirement is formalized in a calculus of information flow and analysed to assess possible conflicts.>