Finding the Best Partitioning Policy for Efficient Verification of Autonomous Systems at Runtime
This work addresses runtime verification challenges for autonomous systems, offering an incremental improvement in model-driven approaches.
The paper tackles the problem of efficiently verifying autonomous systems at runtime by proposing a policy-based analysis approach that finds the best partitioning policy using Balancing and Variation metrics, with experimental results confirming its effectiveness in a case study on energy harvesting systems.
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.