Runtime verification in uncertain environment based on probabilistic model learning.

Area of Science:

• Computer Science
• Software Engineering
• Formal Methods

Background:

• Runtime verification (RV) detects temporal errors by analyzing system execution traces, avoiding state explosion.
• Existing predictive RV methods fail when system models or code are unavailable or environments are uncertain.
• Traditional RV uses multi-valued logic, lacking accurate quantitative correctness descriptions for inconclusive states.

Purpose of the Study:

• To develop a novel runtime verification method for quantitative prediction of temporal property satisfaction.
• To address limitations of existing RV approaches in scenarios with unavailable models or uncertain environments.
• To provide early warnings for potential system failures by predicting correctness probabilities.

Main Methods:

• Learns a probabilistic model (Hidden Markov Model, HMM) from historical traces, transforming it into a Discrete Time Markov Chain (DTMC).
• Translates the Linear Temporal Logic (LTL) property into a Deterministic Rabin Automaton (DRA).
• Generates a probabilistic monitor by computing the product of the DTMC and DRA, calculating state probabilities.

Main Results:

• A probabilistic runtime monitor is generated, providing quantitative predictions of temporal property satisfaction.
• The method enables early detection of potential violations by monitoring correctness probabilities against a threshold.
• Experimental validation on a Unmanned Aerial Vehicle (UAS) simulation platform demonstrates the method's effectiveness.

Conclusions:

• The proposed RV method offers a robust solution for quantitative correctness prediction, even without system models or in uncertain environments.
• Probabilistic monitoring allows for proactive system adjustments by providing advance warnings of potential issues.
• The approach enhances system reliability through early error detection and mitigation strategies.