An Efficient Dynamic Verification Toolkit for Self-Adaptive Systems Addressing Runtime System Model Changes

This repository is an improved version of our former program, “DynaVerify: A Toolkit for Run-time Verification of Self-adaptive Systems Supporting Dynamic Model Changes.” This toolkit aims to implement run-time efficient model checking research, especially under unpredictable environmental changes that lead to updates of the system model. Requirements: - Java SE 17 or later (JRE is required to run the toolkit; it is not bundled with this release). Dependencies: - Jama (public domain)- Java Object Layout (jol-core, Apache License 2.0) Features and APIs Feature 1: Design-time Preprocessing The toolkit performs necessary preprocessing based on the given system model and system requirements at design-time. void designtimeProcess(String Filename) DescriptionLoads and preprocesses the base system model created at design-time. Parameters filename (String): Path to the directory containing the base system model (e.g., ./baseModel.txt) ReturnsNone void setRequrement(double prob) DescriptionSets the system requirement as the minimum required probability of reaching a success state. Parameters prob (double): Threshold value for the reachability probability ReturnsNone Feature 2: Run-time Verification The toolkit performs dynamic verification by substituting observed parameter variable values to a verification formula at run-time. boolean verify(double p[]) DescriptionSubstitutes run-time observed parameter values into the verification formula and evaluates whether the system requirements are satisfied. Parameters p (double[]): Array of observed parameter values at run-time (one value per parameter) Returns boolean: Verification result indicating whether the system requirements are satisfied under the current parameter values Feature 3: Re-generation of Verification Formulae The toolkit regenerates the verification formula based on the given changed system model at run-time. void rutimeProcess(String Filename) DescriptionLoads the updated system model reflecting run-time environmental changes and regenerates the verification formula. Parameters filename (String): Path to the directory containing the updated system model (e.g., ./adaptionModel.txt) ReturnsNone Repository Contents: This repository includes the following files: - toolkit.jar: The main toolkit executable.- baseModel.txt: Example base system model for design-time processing.- adaptionModel.txt: Example updated system model for run-time verification. Notes: This repository is currently under active development. Additional documentation and detailed usage examples will be added soon. If you have any questions or encounter any issues, please feel free to contact us via email.