Understandable and Reusable Formal Verification for Cyber-Physical Systems
Abstract
Air Force cyber-physical systems (CPS), such as manned and unmanned aerial systems (UAS) and satellite constellations, rely on the correct operation of numerous novel and legacy subcomponents over many versions during possibly decades-long lifespans. Understanding and reusing verification results and artifacts across design iterations and abstraction layers in CPS is an unaddressed challenge that the proposed research will address by building on fundamental results for verification reuse in digital logic design and purely software systems and by alleviating the state-space explosion problem. The formal verification will ensure CPS meet their design and mission requirements and only these. Understandable and reusable verification for CPS will enable the Air Force to more reliably, efficiently, and cost-effectively meet the goal to fly, fight, and win … in air, space, and cyberspace.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 09, 2018
- Source ID
- FA95501810122
Entities
People
- Taylor T. Johnson
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- Vanderbilt University