AFChecker Research Project Home

Effective Model Checking for Context-Aware Pervasive Applications

Many smartphone applications leverage the phones' sensors to continously sense and adapt to the users' environment. These context-aware applications typically rely on user-configured rules to customize their behavior. However, evidences [2][3] show that these applications are vulnerable to abnormal adaptations caused by rule misconfigurations. Consider a very simple application that can help users switch their phones between the "silent" and "ring" mode. Users can configure the following two rules:

  • Rule 1: Enable silent mode when a Bluetooth device "OfficePC" is discovered nearby.
  • Rule 2: Enable ring mode when the phone's GPS module reports its current location as "Home".
If the user takes his office PC home for work, the application will discover that both of the two rules are satisfied. If the rules have the same priority level, they would be non-deterministically selected for execution, resulting in an unexpected adaptation. In reality, rule misconfigurations are very common since it is unrealistic to ask users to perform careful rule validation especially when rules are correlated with each other. To automate the rule validation process, researchers [2] have proposed a useful technique (A-FSM). The technique extracts a finite state machine from the user-configured rules, and exhastively searches the state machine's state space to find commonly occurred adaptation faults: (1) underministic adaptation, (2) dead rule predicate, (3) dead state, (4) adaptation race, and (5) unreachable states.

Our Motivation 

Despite that the A-FSM technique will not miss any fault, it could report many false alarms, which seriously affects the technique's usefulness. The goal of our project is to improve the effectiveness of the A-FSM technique. We address the false alarm issue by inferring a domain model and an environment model for a rule-base context-aware application. The models capture the hidden features inside the user-configured rules as well as the application's running environment. We formulate such derived features as detereministic constraints and probabilistic constraints to prune the false alarms and effectively prioritize the fault reports. Therefore, the fault reports generated by our technique would mostly contain true faults or have most true faults  ranked at the very top. By this, the users can quickly realize the misconfigurations in their rules after applying our technique.  

AFChecker Tool

We built our technique as a publically available tool called "AFChecker". AFChecker can work in two modes: non-interactive mode and interactive mode. In non-interactive mode, AFChecker verifies the input finite state machine and reports all detected faults to users. In interactive mode, users can check faults one by one and provide the information that whether the fault is a true fault or not. Based on users' feedbacks, AFChecker would adjust the prioritization of the remaining faults, and report the faults that are most likely to be true to users in the next. Currently, our AFChecker can help verify the applications with rules expressed in a typical form supported by many real-world applications:
  • Rule := <current state, predicate, new state, actions, and priority level>
The predicate can be expressed in a disjunctive normal form with the following syntax:
  • Predicate := Clause | Clause v Predicate
  • Clause := Atom | ┬ČAtom | (Atom ^ Clause)
  • Atom := proposition(context variable)

For details about the capability of our technique, please refer to our reseach paper [1]. We also provide a tutorial page to demonstrate how to use our AFChecker tool. 


  1. Liu Y., Xu, C., and Cheung, S.C. AFChecker: Effective Model Checking for Context-aware Pervasive Applications. The Journal of Systems and Software.
  2. Sama, M., Elbaum, S., Raimondi, F., Rosenblum, D.S., and Wang, Z. 2010a. Context-aware Adaptive Applications: Fault Patterns and Their Automated Identification. IEEE Transactions on Software Engineering 36, 5 , 644-661. 
  3. Tasker Limitations. URL: