Abstract: Problem frames and assurance cases are two current research areas that can improve – and have improved – system dependability, in critical and noncritical systems alike. While these two techniques are effective separately, their synthesis is much more powerful. This paper describes the synthesis of these two techniques and the rationale behind the synthesis, the particular pieces that influence each other, and the beginning of a process to integrate the two in software system development. A detailed example of the application of the synthesis is also provided.

Assurance based development (ABD) is the synergistic construction of a critical computing system and an assurance case that sets out the dependability claims for the system and argues that the available evidence justifies those claims. Co-developing the system and its assurance case helps software developers to make technology choices that address the specific dependability goal of each component. This approach gives developers: (1) confidence that the technologies selected will support the system's dependability goal and (2) flexibility to deploy expensive technology, such as formal verification, only on components whose assurance needs demand it. ABD simplifies the detection - and thereby avoidance - of potential assurance difficulties as they arise, rather than after development is complete. In this paper, we present ABD together with a case study of its use.

In many software systems, properties necessary for dependable operation are only a small subset of all desirable system properties. Assuring properties over the simpler subset can provide assurance of critical properties over the entire system. This work provides a method for constructing systems to be dependably reconfigurable. A system's primary function can have less demanding dependability requirements than the overall system because the system can reconfigure to some simpler function. Reconfiguration thus controls the effective complexity of the system without forcing that system to sacrifice desired, but unassurable, capabilities. Focusing a system's dependability argument on reconfiguration means that reconfiguration must proceed correctly with very high assurance. The system construction approach in this work also provides a method through which system dependability properties can be shown. To illustrate the ideas in this work, we have built part of a hypothetical avionics system that is typical of what might be found on an unmanned aerial vehicle

Hardware dependability improvements have led to a situation in which it is sometimes unnecessary to employ extensive hardware replication to mask hardware faults. Expanding upon our previous work on assured reconfiguration for single processes and building upon the fail-stop model of processor behavior, we define a framework that provides assured reconfiguration for concurrent software. This framework can provide high dependability with lower space, power, and weight requirements than systems that replicate hardware to mask all anticipated faults. We base our assurance argument on a proof structure that extends the proofs for the single-application case and includes the fail-stop model of processor behavior. To assess the feasibility of instantiating our framework, we have implemented a hypothetical avionics system that is representative of what might be found on an unmanned aerial vehicle.

Safe operation is crucial to safety-critical systems, and formal verification of implementations is a desirable means to increase confidence in safety. Traditional formal verification approaches follow the Floyd-Hoare style, setting up a direct compliance argument between an abstract formal specification and a concrete implementation. Such approaches require proofs of large numbers of verification conditions. Creation of both the conditions and their proofs can be difficult and time-consuming.In this paper, we introduce a general formal verification approach that closely models the Floyd-Hoare pattern, yet avoids the tedious direct compliance proof between the formal specification and the implementation. The approach moves the major proof step to a point between two abstract specifications.Our preliminary approach verifies SPARK Ada implementations against PVS specifications. We first use a human-guided refinement to manually generate Ada code along with appropriate SPARK annotations from a PVS specification. We then verify the annotations' compliance with the specification by (1) mechanically extracting a PVS specification from them, and (2) proving that properties of the generated specification imply all of the properties of the original. We rely on the existing SPARK toolset to verify the Ada code against the SPARK annotations. The process is largely automatic or computer-aided. We present an example of the approach using a hypothetical avionics system.

It is often the case that safety-critical systems have to be reconfigured during operation because of issues such as changes in the systems operating environment or the failure of software or hardware components. Operational systems exist that are capable of reconfiguration, but previous research and the techniques employed in operational systems for the most part either have not addressed the issue of assurance or have been developed in an ad hoc manner. In this paper we present a comprehensive approach to assured reconfiguration, providing a framework for formal verification that allows the developer of a reconfigurable system to use a set of application-level properties to show general reconfiguration properties. The properties and design are illustrated through an example from NASA's runway incursion prevention system.