AFChecker Research Project Home

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.

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.
fault fault illustration

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.