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 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 this research addresses by building on fundamental results for verification reuse in digital logic design and in purely software systems and by alleviating the state-space explosion problem. Such formal verification can ensure CPS meet their design and mission requirements and only these. Understandable and reusable verification for CPS can help address major shortcomings in current verification and validation (V and V) processes.

Document Details

• Document Type: Technical Report
• Publication Date: Sep 03, 2021
• Accession Number: AD1154818

Entities

People

• Taylor T. Johnson

Organizations

• Vanderbilt University

Tags

Communities of Interest

• Autonomy
• Cyber

DTIC Thesaurus Topics

• Air Force
• Air Force Research Laboratories
• Artificial Intelligence
• Artificial Intelligence Computing
• Artificial Intelligence Software
• Automata Theory
• Computational Science
• Computer Programming
• Computer Science
• Computers
• Control Systems
• Cyber-Physical Systems
• Electric Power Distribution
• Engineering
• Equations
• Hybrid Systems
• Information Systems
• Internet Of Things
• Neural Networks
• Recurrent Neural Networks
• Scientific Research
• Software Development
• Unmanned Aerial Systems
• Unmanned Systems

Fields of Study

• Computer science
• Engineering

Readers

• Computational Modeling and Simulation
• Database Systems and Applications
• Systems Analysis and Design

Technology Areas

• Autonomy
• Autonomy - Autonomous System Control
• Cyber
• Space