Research Summaries

Back Runtime Verification of Complex Probabilistic Agent-Based Systems

Fiscal Year 2014
Division Graduate School of Operational & Information Sciences
Department Computer Science
Investigator(s) Drusinsky, Doron
Sponsor Defense Threat Reduction Agency (DoD)
Summary 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.
Keywords
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