AFChecker Research Project
Home
Contact: andrewust@cse.ust.hk
Contact: andrewust@cse.ust.hk
Researchers
How to user AFChecker to detect adaptation faults?
AFChecker takes as input
a collection of adaptation rules configured by users and outputs a list
of detected adaptation faults. AFChecker can work in two mode: (1)
Non-interactive mode and (2) interactive mode. In non-interactive mode,
AFChecker prioritizes a list of possible faults and presents them to
users. In interactive mode, AFChecker allows users to check the faults
one by one, and dynamically prioritize the remaining faults based on
users' feedbacks. We use a simple example to demonstrate how to use
AFChecker in this page. More information is covered in the documentation page.
We use the adaptation rules shown in the above table as an example. To use AFChecker, one needs to create a new instance of the Verifier class and feed the adaptation rules' corresponding state machine to the Verifier instance. In our tool, there are two ways to input such a state machine.
The above two methods provide easy ways for context-aware application developers to integrate AFChecker to their applications. After constructing the state machine, to use AFChecker for adaptation fault detection is very easy.
For more enquiries about how to use AFChecker, please read the documentation or contact us.
1. Example Adaptation Rules
We use the adaptation rules shown in the above table as an example. To use AFChecker, one needs to create a new instance of the Verifier class and feed the adaptation rules' corresponding state machine to the Verifier instance. In our tool, there are two ways to input such a state machine.
1.1 Constructing State Machine from Atomic Propositions
In our AFChecker, rules are recursively constructed from atomic propositions. Rules are the main skeleton of the state machine. So the first way is to use the APIs in AFChecker to construct the state machine from atomic propositions as shown in the code snippet.1.2 Constructing State Machine from XML Files
We also provide a easy-to-use parser to construct a state machine from an XML file. Check the file for desribing the rules in the above table. Then we can construct a state machine by calling StateMachineParser.parse(String path) API.The above two methods provide easy ways for context-aware application developers to integrate AFChecker to their applications. After constructing the state machine, to use AFChecker for adaptation fault detection is very easy.
2. Model Checking using AFChecker
AFChecker can work in two modes depending on whether the environment data is provided. If the environemnt data is not provided, AFChecker can only prune false alarms by deriving deterministic constraints (internal correlations between atomic propositions), and works in a non-interactive mode. If the environemnt data is provided, AFCheker will derive probabilistic constraints from the environment data and can work in the interactive mode.2.1 Non-interactive Working Mode
By default, AFChecker works in the non-interactive working mode. After constructing the state machine and verifer, one can simply call the Verifier.verify() API to start checking the state machine model. AFChecker would outputs all detected faults. For example, it will output a fault as shown below (left). The fault report describes the adaptation cycle between the Home state and Outdoor state. |
 |
2.2 Interactive Working Mode
To enable the interactive working mode. One needs to (1) provide a set of environment data for AFChecker to infer an environment model, and (2) set the last boolean flag of the Verifier.verifier() API's parameters to true. The environment data can be feeded into AFChecker using Verifier.setEnvironmentData() API. We also provide a parser for retrieving a list of environment data specified in an XML file. Please check our documentation for more details. In interactive working mode, AFChecker outputs fault reports one by one. Users can confirm the validity of each fault (as shown in the figure below). Based on this feedback, AFChecker would update the environment model (probabilistic constraints) and re-prioritize the remaning faults.For more enquiries about how to use AFChecker, please read the documentation or contact us.