Runtime Monitoring and Verification of Systems with Hidden Information

Abstract

This paper describes a technique for Run-time Monitoring (RM) and Run-time Verification (RV) of systems with invisible events and data artifacts. Our approach combines well-known Hidden Markov Model (HMM) techniques for learning and subsequent identification of hidden artifacts, with run-time monitoring of probabilistic formal specifications. The proposed approach entails a process in which the end-user first develops and validates deterministic formal specification assertions, and then identifies hidden artifacts in those assertions. Those artifacts induce the state set of the identifying HMM. HMM parameters are learned using standard frequency analysis techniques. In the verification or monitoring phase, the system emits visible events and data symbols which are used by the HMM to deduce invisible events and data symbols and sequences thereof. Both types of symbols are then used by a probabilistic formal specification assertion to monitor or verify the system.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 2012
Accession Number
ADA557487

Entities

People

  • Doron Drusinsky

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • Biomedical
  • Cyber
  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Algorithms
  • Artifacts
  • Automata Theory
  • Automated Speech Recognition
  • Computational Science
  • Computer Programming
  • Hidden Markov Models
  • Markov Models
  • Models
  • Probabilistic Models
  • Probability
  • Probability Distributions
  • Random Variables
  • Specifications
  • Standards
  • Validation
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Mathematical Modeling and Probability Theory.
  • Neural Network Machine Learning.
  • Software Engineering.