LIGHTWEIGHT VERIFICATION AND VALIDATION OF CYBERPHYSICAL SYSTEMS USING MACHINE-LEARNED CORRECTNESS PROPERTIES
Authors
Litton, Matthew L.
Subjects
verification and validation
cyberphysical systems
autonomous systems
formal methods
machine learning
cyberphysical systems
autonomous systems
formal methods
machine learning
Advisors
Drusinsky, Doron
Date of Issue
2024-09
Date
Publisher
Monterey, CA; Naval Postgraduate School
Language
Abstract
Conducting verification and validation of autonomous cyberphysical systems is a critical step in facilitating their integration in society and certifying their use by the Department of Defense. However, traditional formal verification and validation techniques are hampered by the necessity of developing formal specifications that capture rigid requirements for system behavior, performance, and dependability. Current approaches for developing formal specifications of systems are complex and error-prone, and they are challenging to apply even for experts. This research demonstrates the feasibility of using machine-learned correctness properties to conduct verification and validation. In addition, advance-notice oracles can be used to predict internal or external faults, proving continuous guarantees of system behavior throughout development, testing, and operating phases.
Type
Thesis
Description
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
166 p.
Citation
Distribution Statement
Distribution Statement A. Approved for public release: Distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.