No abstract available.

The explosive growth in the worldwide use of Unmanned Aerial Vehicles (UAVs) has raised a critical concern with respect to the adequate management of their ad hoc network configuration as required by their mobility management process. As UAVs migrate among ground control stations, associated network services, routing and operational control must also rapidly migrate to ensure a seamless transition. In this paper, we present a novel, lightweight and modular architecture which supports high mobility and situational-awareness through the application of Software Defined Networking (SDN) and Network Function Virtualization (NFV) principles on top of the UAV infrastructure. By combining SDN+NFV programmability we can achieve a robust migration of UAV-related network services, such as network monitoring and anomaly detection as well as smooth UAV migration that confronts high mobility requirements. The proposed container-based monitoring and anomaly detection Network Functions (NFs) as employed within our architecture can be tuned to specific UAV types providing operators better insight during live, high-mobility deployments. We evaluate our architecture against telemetry from over 80 flights from a scientific research UAV infrastructure showing our ability to tune and detect emerging challenges.

We describe the use of model-driven development for safety assurance of a pioneering NASA flight operation involving a fleet of small unmanned aircraft systems (sUAS) flying beyond visual line of sight. The central idea is to develop a safety architecture that provides the basis for risk assessment and visualization within a safety case, the formal justification of acceptable safety required by the aviation regulatory authority. A safety architecture is composed from a collection of bow tie diagrams (BTDs), a practical approach to manage safety risk by linking the identified hazards to the appropriate mitigation measures. The safety justification for a given unmanned aircraft system (UAS) operation can have many related BTDs. In practice, however, each BTD is independently developed, which poses challenges with respect to incremental development, maintaining consistency across different safety artifacts when changes occur, and in extracting and presenting stakeholder specific information relevant for decision making. We show how a safety architecture reconciles the various BTDs of a system, and, collectively, provide an overarching picture of system safety, by considering them as views of a unified model. We also show how it enables model-driven development of BTDs, replete with validations, transformations, and a range of views. Our approach, which we have implemented in our toolset, AdvoCATE, is illustrated with a running example drawn from a real UAS safety case. The models and some of the innovations described here were instrumental in successfully obtaining regulatory flight approval.

We describe dynamic safety cases, a novel operationalization of the concept of through-life safety assurance, whose goal is to enable proactive safety management. Using an example from the aviation systems domain, we motivate our approach, its underlying principles, and a lifecycle. We then identify the key elements required to move towards a formalization of the associated framework.

Safety cases are among the state of the art in safety management mechanisms, providing an explicit way to reason about system and software safety. The intent is to provide convincing, valid, comprehensive assurance that a system is acceptably safe for a given application in a defined operating environment, by creating an argument structure that links claims about safety to a body of evidence. However, their construction is a largely manual, and therefore a time consuming, error prone, and expensive process. We present a methodology for automatically assembling safety cases which are auto-generated from the application of a formal method to software, with manually created safety cases derived from system safety analysis. Our approach emphasizes the heterogeneity of safety-relevant information, and we show how diverse content can be integrated into a single argument structure. To illustrate our methodology, we have applied it to the Swift Unmanned Aircraft System (UAS) being developed at the NASA Ames Research Center. We present an end-to-end fragment of the resulting interim safety case comprising an aircraft-level argument manually constructed from the safety analysis of the Swift UAS, which is automatically assembled with an auto-generated lower-level argument produced from a formal proof of correctness of the safety-relevant properties of the software autopilot.

Software plays a key role in high-risk systems, i.e., safety and security-critical systems. Several certification standards and guidelines, e.g., in the defense, transportation (aviation, automotive, rail), and healthcare domains, now recommend and/or mandate the development of assurance cases for software-intensive systems. As such, there is a need to understand and evaluate (a) the application of assurance cases to software, and (b) the relationship between the development and assessment of assurance cases, and software engineering concepts, processes and techniques. The ICSE 2013 Workshop on Assurance Cases for Software-intensive Systems (ASSURE) aims to provide an international forum for high-quality contributions (research, practice, and position papers) on the application of assurance case principles and techniques for software assurance, and on the treatment of assurance cases as artifacts to which the full range of software engineering techniques can be applied.

We describe our experience with the ongoing development of a safety case for an unmanned aircraft system (UAS), emphasizing autopilot software safety assurance. Our approach combines formal and non-formal reasoning, yielding a semi-automatically assembled safety case, in which part of the argument for autopilot software safety is automatically generated from formal methods. This paper provides a discussion of our experiences pertaining to (a) the methodology for creating and structuring safety arguments containing heterogeneous reasoning and information (b) the comprehensibility of, and the confidence in, the arguments created, and (c) the implications of development and safety assurance processes. The considerations for assuring aviation software safety, when using an approach such as the one in this paper, are also discussed in the context of the relevant standards and existing (process-based) certification guidelines.

Safety cases capture a structured argument linking claims about the safety of a system to the evidence justifying those claims. However, arguments in safety cases tend to be predominantly qualitative. Partly, this is attributed to the lack of sufficient design and operational data necessary to measure the achievement of high-dependability goals, particularly for safety-critical functions implemented in software. The subjective nature of many forms of evidence, such as expert judgment and process maturity, also contributes to the overwhelming dependence on qualitative arguments. However, where data for quantitative measurements can be systematically collected, quantitative arguments provide benefits over qualitative arguments in assessing confidence in the safety case. In this paper, we propose a basis for developing and evaluating the confidence in integrated qualitative and quantitative safety arguments. We specify a safety argument using the Goal Structuring Notation (GSN), identify and quantify uncertainties therein, and use Bayesian Networks (BNs) as a means to reason about confidence in a probabilistic way. We illustrate our approach using a fragment of a safety case for an unmanned aircraft system (UAS).

Automated code generators are increasingly used in safety-critical applications, but since they are typically not qualified, the generated code must still be fully tested, reviewed, and certified. For mathematical and engineering software this requires reviewers to trace subtle details of textbook formulas and algorithms to the code, and to match requirements (e.g., physical units or coordinate frames) not represented explicitly in models or code. We support these tasks by using the AutoCert verification system to identify and verify mathematical concepts in the code, recovering verified traceability links between concepts, code, and verification conditions. We then exploit these links to construct a natural language report that provides a high-level structured argument explaining where the code uses specified assumptions and why and how it complies with the requirements. We have applied our approach to generate review documents for several sub-systems of NASA's Project Constellation.

Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the meta-program fragments for annotation construction. However, this is difficult since it involves tedious and error-prone low-level term manipulations.

Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e., pre- and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains difficult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator).Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property-specific abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding definitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.

Automated code generation offers many advantages over manual software development but treating generators as trusted black boxes raise problems for certification. Traditional process-oriented approaches to certification thus require that the generator be verified to the same level of assurance as the generated code, but this is infeasible for realistic generators. However, generators can be extended to support an evidence-based approach to certification. By careful design of the trusted kernel, assurance of the generator itself is not required. In this paper, we describe several related extensions to two in-house code generators to provide two forms of evidence along with the code: safety proofs and safety explanations. We also describe how additionally provided links are used to trace between the code and the safety artifacts.

Automated code generation is an enabling technology for model-based software development and promises many benefits, including higher quality and reduced turn-around times. However, the key to realizing these benefits is generator correctness: nothing is gained from replacing manual coding errors with automatic coding errors. In this paper, we describe an alternative technique that uses a generic post-generation annotation inference algorithm. We exploit both the highly idiomatic structure of automatically generated code and the restriction to specific safety properties. Since generated code only constitutes a limited subset of all possible programs, the new "eureka" insights required in general remain rare in our case. Since safety properties are simpler than full functional correctness, the required annotations are also simpler and more regular. We can thus use patterns to describe all code constructs that require annotations and templates to describe the required annotations. We use techniques similar to aspect-oriented programming to add the annotations to the generated code: the patterns correspond to (static) point-cut descriptors, while the introduced annotations correspond to advice. The annotation inference algorithm can run completely separately from the generator and is generic with respect to the safety property, although we use initialization safety as running example here. It has been implemented and applied to certify initialization safety for code generated by Auto-Bayes and AutoFilter

The goal of this workshop is to explore new technologies, underlying principles, and general methodologies for supporting software certificate management. Software certification demonstrates the reliability, safety, or security of software systems in such a way that it can be checked by an independent authority with minimal trust in the techniques and tools used in the certification process itself. It can build on existing validation and verification (V&V) techniques but introduces the notion of explicit software certificates, which contain all the information necessary for an independent assessment of the demonstrated properties. Software certificates support a product-oriented assurance approach, combining different techniques and forms of evidence (e.g., fault trees, "sign-offs", safety cases, formal proofs, ...) and linking them to the details of the underlying software. A software certificate management system provides the infrastructure to create, maintain, and analyze software certificates. It combines functionalities of a database (e.g., storing and retrieving certificates) and a make-tool (e.g., incremental re-certification). It can also maintain links between system artifacts (e.g., design documents, engineering data sets, or programs) and different varieties of certificates, check the validity of certificates, provide access to explicit audit trails, enable browsing of certification histories, and enforce system-wide certification and release policies. It can at any time provide current information about the certification status of each component in the system, check whether certificates have been audited, compute which certificates remain valid after a system modification, or even automatically start an incremental recertification.

We describe the development of a Java bytecode optimisation algorithm by the methodology of program extraction. We develop the algorithm as a collection of proofs and definitions in the Coq proof assistant, and then use Coq's extraction mechanism to automatically generate a program in OCaml. The extraction methodology guarantees that this program is correct. We discuss the feasibility of the methodology and suggest some improvements that could be made.