Finding the Best Partitioning Policy for Efficient Verification of Autonomous Systems at Runtime

TL;DR

This paper introduces a policy-based method for partitioning models to improve runtime verification efficiency of autonomous systems, using metrics to select optimal partitions and validated through theoretical analysis and experiments.

Contribution

It proposes a novel policy-based analysis approach with metrics for optimal model partitioning, enhancing verification efficiency for autonomous systems at runtime.

Findings

The approach effectively balances model size and change frequency.

Experimental results confirm improved verification efficiency.

Theoretical validation supports the approach's correctness.

Abstract

The autonomous systems need to decide how to react to the changes at runtime efficiently. The ability to rigorously analyze the environment and the system together is theoretically possible by the model-driven approaches; however, the model size and timing limitations are two significant obstacles against such an autonomous decision-making process. To tackle this issue, the incremental approximation technique can be used to partition the model and only verify a partition if it is affected by the change. This paper proposes a policy-based analysis approach that finds the best partitioning policy among a set of available policies based on two proposed metrics, namely Balancing and Variation. The metrics quantitatively evaluate the generated components from the incremental approximation scheme according to their size and frequency. We investigate the validity of the approach both theoretically and experimentally via a case study on energy harvesting systems. The results confirm the effectiveness of the proposed approach.