Understandable and Reusable Formal Verification for Cyber-Physical Systems
This project entitled "Verification of Autonomous Systems" sponsored by the Air Force Office of Scientific Research, is looking at ways to formally verify that systems that may operate on their own or autonomously meet their requirements.
SHF: Small: Collaborative Research: Fuzzing Cyber-Physical System Development Tool Chains with Deep Learning (DeepFuzz-CPS)
Developing a modern technical product such as a car, plane, or a complex medical device includes designing the complex interplay between sensors (which measure physical product and environment state) and actuators (such as small electric motors that control the product).
FMitF: Track II: Hybrid and Dynamical Systems Verification on the CPS-VO
This project aims to transition recent research results that automate portions of the verification process of Cyber-Physical Systems into broader practice, particularly with industrial and student users. Cyber-physical systems (CPS) are networked embedded computing systems coupled with physics, such as in motor vehicles, aircraft, medical devices, and the electrical grid.
Collaborative Research: Operator theoretic methods for identification and verification of dynamical systems
Widespread use of automation in many sectors of society has yielded a large amount of data regarding historical behaviors for a variety of dynamical systems, such as unmanned aerial, marine, and ground vehicles, biological systems, and weather systems. This project aims to develop novel algorithms to discover governing rules that explain the observed behaviors (i.e., trajectories) of dynamical systems. Discovery of underlying models, while useful for analysis and control, can be computationally challenging.
CODES: Compositional DSLs for Enhancing Software
The goal of this project is to study how domain-specific languages (DSLs) can be used to represent components of legacy systems and to use the DSLs to enhance those components. The project involves formal methods, compilers, and program analysis, such as symbolic execution.
Model-based Intent-Driven Adaptive Software (MIDAS)
The project’s goal is to develop a new approach to evolutionary software development and deployment that extends the results of model-based software engineering and provides an integrated, end-to-end framework for building software that is focused on growth and adaptation.
Assurance-based Learning-enabled Cyber-Physical Systems (ALC)
Autonomous vehicles (cars, drones, underwater vehicles, etc.) have started using software components that are built using machine learning techniques. This is due to the fact that these vehicles must operate in highly uncertain environments and that we cannot design a correct algorithm for all possible situations.