Model-Based Compositional Reasoning for Complex Systems of Systems

ABSTRACT: The proposed research builds on Dependable Computing's successful Phase I effort. The Phase II effort demonstrates the critical role played by the system safety case in the development of complex systems of systems. Specifically, the safety case (1) informs and guides systems and safety engineering and (2) enables compositional certification through use of contract-adapter arguments. Additionally, the Phase II effort demonstrates the role that the system-interface abstraction technology plays in the design and analysis of complex systems of systems. Specifically, the system-interface abstraction technology (1) formalizes critical context in the safety case, (2) hides details about component-system behaviors, (3) informs decomposition of claims in the safety case, and (4) allows formal proofs to be established for compositional properties of the system of systems. Finally, the Phase II effort is supported by novel tools designed to prepare the approach for commercialization. The safety case, technology and tools are demonstrated by application to the VIPERS challenge problem in the development of a VIPERS testbed. The effort culminates in flight testing of representative VIPERS assets. BENEFIT: Systems of systems provide a major and growing challenge to the state of the art in safety assurance. Individual systems are becoming increasingly complex, and are being combined in larger numbers and in more sophisticated ways as functionality escalates. There are significant opportunities for the application of the proposed technology within both the defense and civilian sectors. The Department of Defense (DoD) has clear and pressing needs for the technology developed under the proposed effort. There is an expanding emphasis on unmanned aircraft systems (UAS) within the DoD. UASs are, by their very nature, complex systems of systems involving: one or more unmanned aircraft; communication systems that typically involve multiple radio links some operating through satellites; and a ground station that incorporates many different discrete systems such as workstations, servers, networks, and displays. The inherent complexity of the UAS requires the kind of formal, compositional reasoning that the proposed effort enables. Crucial properties at the system of systems level can only be established by formal means because of the large number of possible system states that have to be analyzed. Existing formal techniques, though powerful, tend to address issues arising only at the system level. From a certification point of view, although they are undocumented, informal and ad hoc, compositional arguments are already in use (e.g., when components that have an FAA Technical Standard Order are used). The compositional safety case makes such reliance rigorous, explicit and reusable. Use of the proposed technology is certainly not limited to UASs or even aviation. Any complex military system of systems (or complex system) will benefit from both the formalization of the system architecture and the compositional reasoning capabilities afforded by the proposed technology. In the civilian sector, the uses of the proposed technology are equally broad; two specific examples are civil aviation and the automotive industry. Civil aviation needs new and more powerful formal analysis techniques to address the scale and complexity of modern aircraft. The series of issues that have plagued the Boeing 787 Dreamliner underscores this point: modern transport aircraft are complex systems that stretch the capabilities of current best practices in safety assurance. An analogy can be drawn between the present situation with safety analysis and the situation with aircraft structural analysis at the time of the development of the Boeing 747 in the 1960s. Comprehensive structural analysis of the B747 was severely limited by computational techniques and capacity. The ability to reason formally over the composition of components and subsystems will benefit the aviation industry. Likewise, compositional safety arguments, enabling compositional certification and recertification, will both control certification costs and allow more-rapid uptake of new safety- and performance-enhancing technologies. As Dependable Computing's related work with our industry partners demonstrates, there is a growing desire in other industries to formally establish assurance of safety. The formal and compositional reasoning that the proposed technology enables will directly benefit these other industries. Likewise, while many other industries are not currently regulated and therefore not subject to certification pressure, demonstration of adherence to voluntarily adopted standards like ISO 26262, which requires a safety argument will be simplified through compositional assurance arguments. Numerous safety-critical industries will benefit from formal reasoning and compositional safety arguments, including: - the medical-device industry, for example drug infusion pumps and radiation treatment machines; - the rail industry, for example in signaling, braking, and separation systems; - the offshore drilling industry, for example in monitoring and control systems; - the nuclear industry, for example in core thermal management and radiation monitoring; and - the shipping industry, for example in navigation, guidance and ship control. In addition to these safety-critical domains, industries for which the economic cost of failure is very high, such as finance and utilities (e.g., power, water, telecommunications), will greatly benefit from formalized compositional reasoning and compositional assurance arguments.