Summaries - Office of Research & Innovation
Back Runtime Verification of Complex Probabilistic Agent-Based Systems
|Division||Graduate School of Operational & Information Sciences|
|Sponsor||Defense Threat Reduction Agency (DoD)|
The base period of performance for MIPR 11-2338M provided theoretical foundations for Runtime Verification (RV) and Runtime Execution Monitoring (REM) of noisy, multi-agent, probabilistic, concurrent, timed and asynchronous sequences systems using a hybrid of UML-based formal specifications, Hidden Markov Models (HMMs), and Kalman filters.
The proposed optional two-year extension effort consists of two tasks. First, we will develop a technique for predictive verification using loosely bounded constraint solving. We will then develop two code generators for UML-based formal specifications: a Java code generator, and a code generator for the MIT-Kodkod constraint solver.
The proposed Java code generator will be based on the algorithms published as a result of the base period of performance. The Kodkod code generator will be applicable for the results of the third and fourth years of this effort. In addition, we are discussing the use of the planned Java code generator by NASA’s Independent Verification and Validation (IV&V) facility.
|Publications||Publications, theses (not shown) and data repositories will be added to the portal record when information is available in FAIRS and brought back to the portal|
|Data||Publications, theses (not shown) and data repositories will be added to the portal record when information is available in FAIRS and brought back to the portal|