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.
References
- Liu Y., Xu, C., and Cheung, S.C. AFChecker: Effective Model
Checking
for Context-aware Pervasive Applications. The Journal of Systems and
Software.
- 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.
- Tasker Limitations. URL:
http://tasker.dinglisch.net/bugs.html