Dagstuhl Seminar 15071 on “Formal Foundations for Networking” brought together researchers and practitioners from the fields of networking, formal methods, programming languages, and security, to investigate key questions relating to the acute need for methods and tools that can provide rigorous guarantees about the behavior, performance, reliability, and security of networked systems. This productive workshop combined talks on challenges and solutions; Prof. Kristin Yvonne Rozier issued a monumental challenge to the community in the talk “Formal Methods Challenge: Efficient Reconfigurable Cockpit Design and Fleet Operations using Software Intensive, Networked, and Wireless-Enabled Architecture (ECON)“.
ABSTRACT: We are at the dawn of a new generation of aircraft! Current aircraft are consistently built over-weight and over-budget and suffer from limitations that cannot carry forward into our increasingly digital age. In order to meet the demands placed on future aircraft, we need to design a new type of *net-enabled* aircraft by reducing aircraft weight, increasing automation and modularity, moving from hardware to software systems, moving from on-board/aircraft-based systems to cloud/fleet-based systems, and thereby facilitating easier and more responsive maintenance and system health management procedures.
For example, the wiring alone on the A-380 weighs approximately six tons, while each ton of weight in the aircraft infrastructure costs an estimated $7.2 billion in fuel across a fleet in the U.S. each year. We ask the question: can we replace some of these wires with wireless systems? Can we add wireless backup systems for wired systems that don’t currently have backups due to weight constraints? But then how do we design these new hybrid systems in a way that allows us to rigorously reason about their safety, reliability, availability, and security? For another example, can we replace heavy, customized, and therefore hard-to-maintain cockpit systems by lighter, more modular, alternatives using wireless, software, or cloud-based technologies? We have not solved the formal verification problem for current cockpits; how will we scale to net-enabled cockpits?
We must reason about an aircraft as a network of avionics sub-systems, about a fleet as a network of aircraft, and about both of these being located in the cloud. What restrictions do we need to make to enable formal verification, from design-time to runtime? Join this NASA-lead team of government, academia, and industry experts as we attempt to answer the ultimate question: how can we design and verify a new class of net-enabled aircraft that are *lighter*, *cheaper*, and *safer* than ever before?