Experiments of Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare

                                           

This webpage is used to give more details of the experiments in Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare. We use our home grown model checker PAT to fulfill these experiments. The following models are verified in our paper.

·         Case Study: Ambient Intelligent System for Elderly Dementia Healthcare

This page is maintained by Liu Yan.

Please contact with us if you have any question about this webpage or these experiments. We will reply your enquiries as soon as possible.

 

Case Study: Ambient Intelligent System for Elderly Dementia Healthcare [1]

The Healthcare system designed for Elderly Dementia is specified in the paper. We model the whole system along with the model of the patient behavior, thus to explore interesting properties of the system.

Explanation of the Files:

There is one system model but three patient models regarding the feasibility of checking the desired properties. We integrated the three patient models with the system model and produce three system models along with its properties in the following:

·         SmartBedroom Model - which reasons about the patients’ behaviors in the bedroom.

·         SmartShowerRoom Model - which reasons about the patients’ behaviors in the shower room.

·         SmartRoom Model - which is a complete model that integrates both the behaviors in the bedroom and the behaviors in the shower room.

There is another file named PAT.Lib.SmartRoom.dll where resides the external C# methods called by the models. These methods basically perform the simple variable updating and calculation. They are shared by all the three models for the purpose of saving the computation power which contributes to solve the state explosion problem in our model. Note:

1. This external C# method is a special feature of our model checker PAT, interesting readers please refer to the PAT manual section 2.5 for more details.

2. If you are going to run the experiment, please put the model file and this dll under the same directory. You are also encouraged to use Verification Batch Mode under the tool tab of our model checker PAT. In case, the system may run for a long time, the batch mode is able to record the result into a text file.

Experiment Results:

As specified along with the models files, there are four categories of properties regarding the deadlock freeness (P1.*), the reminder effectiveness (P2.*), the inconsistency within the system (P3) and the false/conflictive reminders (P4.*). The verification is run on a PC with the CPU of Intel(R) Xeon(R) CPU E5506 @2.13GHz 2.13GHz (2 processors) and 32 GB memory.

For the detailed description of the properties, please refer to the respective model file.

Property

Details

Result

#States

#Transitions

Execution Time(s)

P1.1

#assert SmartRoom deadlockfree;

-

-

-

Out Of Memory

P1.2

#assert SmartBedroom() deadlockfree;

True

1433654

2038064

815

P1.3

#assert SmartShowerRoom() deadlockfree;

True

10783353

15832370

7045

P2.1

#assert SmartBedroom() |= [](UsingWrongBed -> <>RemindedWrongBed);

True

1599797

2430351

1945

P2.2

#assert SmartShowerRoom() |= [](TapNotOff -> <>OffTapReminded);

False

68178

130734

39

P2.3

#assert SmartShowerRoom() |= [](WanderingInShowerRoom -> <> WanderReminded);

False

2192251

4531005

12414

P2.4

#assert SmartShowerRoom() |= [](ShowerWithoutSoap -> <>NoSoapReminder);

False

832144

1663779

729

P2.5

#assert SmartShowerRoom() |= [](ShowerTooLong -> <> EndShowerReminded);

False

4314

5150

1.6

P2.6

#assert SmartBedroom() |= [](TroubleSleep -> <>RemindedSleep);

True

1579579

2377381

1913

P3

#assert SmartShowerRoom() reaches InConsistency;

True

572

745

0.3

P4.1

#assert SmartShowerRoom() reaches ConflictReminderSR;

True

14675

20615

6.1

P4.2

<#assert SmartBedroom() reaches FalseAlarm;

True

2446

3036

1.11

P4.3

#assert SmartRoom reaches ConflictReminderH1;

True

2332744

3001756

1047

 

Discussion:

1.       Explanation for the result for each property:

·         P1.1: This property is to check the deadlock freeness of the complete system model including the patients’ behaviors both in the Bedroom and Shower room. However, the state space of this model is expected to be of 10^15 states which is beyond the upper limit of our PAT model checker.

·         P1.2: This property is to check the deadlock freeness of the system model integrated with the patient behavior model in the bedroom. And it is free of deadlocks.

·         P1.3: This property is similar with P1.2. The only difference is that this SmartShowerRoom model contains the patient behavior model in the shower room. And it is also free of deadlock. The statistic also shows the model has the state space at the level of 10^8 which reaches the upper bound of PAT model checker.

·         P2.1 and P2.6: They are liveness properties defined against the effectiveness of the reminders in the bedroom. They are valid which shows the system is well behaved that it will send the reminder anytime there is needed.

·         P2.2 to P2.5: They are liveness properties defined against the effectiveness of the reminders in the shower room. Interestingly they are all failed. Details will be discussed next in the Bug Report.

·         P3: The abnormal state defined in P3 is reachable revealing the inconsistency within the system.

·         P4.1 to P4.3: These are undesired behaviors of the reminders that they could conflict each other or send to the wrong person. These defined situation are all reachable witnessed the scenarios explained below.

·         Note: P4.3 is not within the paper due to the limited space. However, it is interesting discovered that even the reminders in the shower room and bedroom can conflict each other. And although the complete model fails to check the deadlock freeness property, it is still able to reveal the system bugs by carefully design the property expressions.

2.      Bug Reported:

·         P2.2 - P2.5: The violation of these properties reveals a similar problem within this system that it fails to update the patient's location when he exits the shower room. However most of the rules are related to the location of the patient. A typical counterexample is if the patients exit the shower room and leave the shower tap on, the rule defined for shower not off and patient wandering will repeatedly activate the two reminders even though there is no patient in the shower room. This counterexample has intuited the reachability checking of the inconsistency within the system as defined in P3 as follows.

·         P3: The inconsistent state is reachable which exposes the system's inability to capture the real location of the patient. The witnessed trace said that the system detects the shower room is empty however the variable which stores the patient's location is remained to shower room. This is a obvious contradiction within the system.

·         P4.1: It is validated by the scenario that the patient first wandered in the shower room and triggered the wander reminder. Then instead of leave the shower room as the wander reminder requires, he turns the shower tap and play with water for a long time that triggers the shower without soap reminder. Since condition for deactivate wander reminder is shower room empty, the wander reminder is activated together with the shower without soap. The two reminders which one asks the patient to leave while the other asks the patient to press soap and continue confuse the patient.

·         P4.2: It is valid that even though the patient with ID 1 is not in the bedroom, somehow the sit bed for too long reminder sends to him falsely. By a careful examine at the system design, we spotted that the rule defined against the sit bed long behavior always sends to the bed owner by default no matter who is sitting on the bed. Even the heavy bag placed on the bed may cause this reminder to send to the patient which is not reasonable.

3.      Observation of the system design:

As an insight in to our experience, we list the following observations in designing such systems. First and foremost, the consistency within the system itself and its environment is critical, especially when the system highly replies on some of the information. For instance, in our case, system failing to keep the location information of the person consistent with the actual environment leads to the violation of the important desired properties. Secondly, to detect the critical location information, it is unwise to solely reply on a single sensor such as RFID reader which is not highly accurate in the same time. This poses a decision of the design team to reduce the dependency on RFID reader. Alternatively, the other techniques such as sound recognition and deduction utilizing the existing knowledge of the system are considered. Additionally, during the experiments we noticed that lots of duplicated messages are sent out by the reasoning engine. This is one cause of the state explosion problem. However, we also believe these duplicated messages brought down the system efficiency and increased the complexity of the system. A smarter reasoning engine needs to be investigated carefully. Finally, mechanisms for deactivation of reminders should be more intelligent and user friendly. Conflicts and false reminders which lead to the confusion of the patients need to be carefully avoided.

4.      Discussion on the State Explosion problem:

Besides the observations made on the system design, the experimental results reflects typical state space explosion problem for model checking techniques. From the table, we can see that the number of states in verifying P1.3 is at the level of 10\^8, which reaches the limitation of explicit-state model checkers like SPIN and PAT. This is caused by the highly concurrent behaviors of the system components. From our point of view, more effective reduction techniques need to be applied such as partial order reduction (POR) [2] or symmetry reduction [3]. However, this is highly nontrivial that some issues should be specially taken care of. For instance, context awareness systems typically involving context update and synchronous events will fail classic POR and symmetry reduction. Furthermore, the heterogeneity of the system components prevents the application of symmetry reduction. Other techniques like Assume-Guarantee model checking techniques can be also applied to alleviate the problem of exploring large state spaces [4].

References

1.      Jit Biswas, Mounir Mokhtari, Jin Song Dong, and Philip Lin Kiat Yap. Mild dementia care at home - integrating activity monitoring, user interface plasticity and scenario verification. In ICOST, pages 160–170, 2010.

2.       D. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV, pages 377–390, 1994.

3.      E. M. Clarke, T. Filkorn, and S. Jha. Exploiting Symmetry In Temporal Logic Model Checking. In Proceedings of the 5th International Conference on Computer Aided Verification(CAV 1993), volume 697 of LNCS, pages 450–462. Springer, 1993.

 

4.       C. S. Pasareanu, M. B. Dwyer, and M. Huth. Assume-guarantee model checking of software: A comparative case study. In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pages 168–183, London, UK, 1999. Springer-Verlag.