The Ninth Layered Assurance Workshop (LAW) brought together academic and industrial researchers to push the bleeding edge of Compositional Trustworthiness.
LAW is affiliated with the Annual Computer Security Applications Conference (ACSAC).
Layered assurance encompasses “diverse manifestations of combined assurance, including composition (of assured components), incremental certification (incremental cost for incremental change), abstraction layers (building upon assurance of lower layers), and polymorphism (common assurance of variants, such as among members of a product line).”
https://www.acsac.org/2015/workshops/law/Rozier-Keynote-LAW2015.pdf
TITLE:
Layers of Formal Verification for Full-Scale NextGen Automated Air Traffic Control
ABSTRACT:
We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that is more scalable while also proving at least as safe. Now that we have the chance to redefine air traffic control from scratch, the question arises: how do we do it safely?
We explore new frontiers in symbolic model checking to scalably answer the functional allocation question: instead of analyzing one design, or comparing a pair of designs, we now need to take into account a large number of permutations and combinations of functions that comprise a large set of possible designs. We compositionally model and comparatively analyze this set with regard to safety on multiple levels, considering the full space of possible system designs both in nominal conditions and in the presence of faults. Our analysis helps NASA narrow the possible design space, saving time and cost of later-phase evaluations, identifying both novel and known problematic design configurations. We look to the future, where a componsitional approach layering different verification techniques at multiple levels will be required to build up a safety case for the final design.