Reusable Formal Verification for Cyber-Physical Systems
Abstract
Software and verification reuse is a cost-effective strategy to update legacy systems and create new systems, however, there have been catastrophic problems in the interoperability of this re-usage; the research proposed would eliminate any interoperability problems and thus ensure warfighting capabilities for our warfighters. A cyber-physical system (CPS) is a system with embedded sensors, processors, and actuators that are designed to sense and interact with the physical world (including users), and support real-time, guaranteed performance in safety-critical applications. So, the juxtaposition of "cyber" elements and "physical" elements is crucial; the CPS s components have computing, control, sensing, and networking, and the actions of the CPS and its components must be safe and interoperable. CPSs include manned and unmanned aerial systems (UAS) and satellite constellations; these CPSs rely on the correct operation of numerous subcomponents over many versions during possibly decades-long lifespans. Reusing verification results and artifacts across design iterations and abstraction layers in CPS is an unaddressed challenge. The proposed research will study the state-space explosion problem and build on previous fundamental results for verification reuse in digital logic design and in purely software systems. The formal verification will ensure CPS meet design and mission requirements. Reusable verification for CPS will enable the Air Force to more reliably, efficiently, and cost-effectively meet DoD mission goals.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jul 15, 2016
- Source ID
- FA95501610246
Entities
People
- Taylor T. Johnson
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Texas at Arlington