Automatic Verification of Nonlinear Systems Without Abstractions Using Continuation Methods
Short Term Aerospace Research and Development Program (STAR-DP), Universal Technology Corporation, Aerospace Systems Directorate of the Air Force Research Laboratory (AFRL)
27 July 2015 - 31 December 2015
Total award: $50,334
One of the most challenging problems in safety assurance of cyber physical systems is handling the structure and complexity of the underlying dynamics. While automated verification techniques such as model checking and theorem proving permit discrete jump and nondeterminism, their application is restricted to a certain class of underlying physical system dynamics. The objective of this research effort is to formulate a new verification technique using continuation methods to eliminate the need for finite state abstraction or construction of differential invariants. Numerical continuation methods deal with the problem of identifying changes in a set of nonlinear equations as system parameters are varied. The major benefit of this computation is simultaneous evaluation of safety criteria and values of critical system parameters. This benefit will be substantiated during the period of performance by pursuing the following research tasks:
- Classify the “changes” in safety requirements under the influence of specific constraint functions.
- Identify and describe the type of constraint functions, scalability and computational cost of current state-of-the-art continuation algorithms.
- Develop a research roadmap that outlines near-term and far-term goals in continuation method based verification including description of potential prototype algorithms.
Working with me on this research is graduate research assistant, Peter Uth.
Rigorous Procedure to Show Compliance with Airworthiness Regulations
Joint Center for Aerospace Technology Innovation
Industry Partner: Certification and Safety Office, Safran Engineering Services
1 July 2015 - 30 June 2016
Total award: $77,097
Current certification methodology for transport category airplanes requires the system to be "fully" tested through combination of wind tunnel and full scale flight tests and Monte Carlo forward time simulations, reaching over 3000-5000 hours. The collaborative effort between Professor Narang, Certification and Safety Office of Safran Engineering Services with Dr. Christine Belcastro (NASA Langley Research Center) as advisor under support from the Joint Center for Aerospace Technology Innovation is focused on inventing an alternate means of showing compliance by leveraging benefits of continuation methods to curtail the developmental costs. The savings from continuation methods are twofold (i) eliminating need for long hours of forward time simulations and (ii) preventing vehicle loss by predicting critical portions in the flight envelope early in the certification process. These savings are being quantified under this support by applying continuation methods to NASA's AirStar 5.5% dynamically scaled aircraft model and comparing its insights with experimental flight test data.
Working with me on this research are graduate research assistants, Armand I. Awad and Max G. Spetzler.