Visualizing Self-Adaptive Plan Simulations given Embedded Verification Concerns

摘要

A system that dynamically self-adapts at runtime, should comply with critical requirements. However, runtime verification is difficult even when the system was originally formulated to expect adaptation and allowable changes are preconfigured or prespecified. Our approach examines verification processes originally performed for compliance with system requirements to identify specific verification concerns, such as variables, safety and liveness property conditions, and architecture properties. The expectation is that if a verification concern is impacted by an adaptation then the reuse of the original verification process may be restricted. If verification process reuse is inhibited, then there is increased likelihood that the requirements relying on that verification concern may no longer be guaranteed. In this demonstration, we illustrate our approach to take identified verification concerns for each requirement and embed them as checkpoints within the code, given the flow of the verification process from which they were derived. Simulating an adaptation plan produces log files based on which checkpoints are reached. Failure to complete a path through the checkpoints without raising a flag indicates that the verification process may not be repeatable and the adaptation plan may be risky to perform. We visualize the paths using ProM which shows where and how an adaptation plan may be problematic.