Embedding Verification Concerns in Self-Adaptive System Code

For a self-adaptive system, adaptive plans deployed at runtime should comply with critical requirements. The ability to assess plans is especially useful when the system operates for long periods without intervention. Dynamic compliance re-verification consumes enormous resources that may not be available. Plus, in many cases, re-verification of all requirements is unnecessary because the adaptive plan does not impact the associated state variables. If a plan can be configured dynamically from predefined parts, one method is to pre-check all possible plan combinations to determine if compliance could be violated. Unfortunately, this approach disallows runtime formulation of new functionality or new functionality integrations for self adaptation. Thus, these new products will not he fully vetted prior to system deployment. However, if the deployed system has been verified to comply with critical requirements, then a verification process exists for each requirement. Our approach focuses on allowing the system to dynamically determine the potential for an adaptive plan to inhibit repeatability of the prior verification processes. If a verification process, such as a proof or certification, cannot he reused, there is a risk that requirement compliance can be violated. Our objective is to abstract verification concerns from the verification process and embed them as checkpoints within the code to provide a form of verification awareness. The checkpoints collect values as an adaptive plan is simulated, which are mined and visualized using Prolyl to determine the plan's potential to limit the reuse of the verification process.