MenShen:Systematically Ensuring The Confidence of Real Time Home Automaton IoT Systems
Introduction Download Case Studies User Studies

Case Studies


Case Studies For MenShen

Results of Applying MenShen To Analyze Different Home Automation IoT Systems (#Devices and #Rules denote the number of devices and rules in the data set, respectively. #LHA denotes the number of generated LHA models. Check denotes the time spent in checking the problem. Fix denotes the time spent in fixing. The default bound we set for all the problem is 10 for all the automata. )

 

System #Devices #Rules Original System System Minimization Related Rules Merging
#LHA Model (s) Check (s) Fix (s) #LHA Model (s) Check (s) Fix (s) #LHA Model (s) Check (s) Fix (s)
SC-1
3
3
6
0.011
0.26
0.98
6
0.011
0.26
0.98
6
0.012
0.26
0.98
SC-2
3
3
6
0.011
0.26
1.25
6
0.010
0.26
1.25
6
0.011
0.26
1.25
SC-3
2
2
4
0.011
0.12
0.66
4
0.011
0.12
0.66
4
0.013
0.12
0.66
SC-4
3
2
5
0.010
0.22
0.92
5
0.013
0.22
0.92
5
0.013
0.22
0.92
MS-1
12
15
27
0.013
1.89
51.17
20
0.012
0.88
3.62
20
0.012
0.92
3.32
MS-2
12
15
27
0.012
1.79
365.58
20
0.013
1.23
8.62
20
0.015
1.02
7.88
MS-3
18
20
38
0.012
3.77
11.19
3
0.017
0.23
0.97
3
0.013
0.23
0.95
MS-4
18
19
37
0.013
3.56
10.50
3
0.012
0.23
0.98
3
0.013
0.23
0.95
ISY
46
65
111
0.014
9.25
1209.4
25
0.024
0.97
7.51
25
0.016
0.52
3.98

 

Notes

1. The experiments are conducted on a Think Center Desktop(Intel Core2 Quad CPU 2.83GHz,4 GB RAM, UBUNTU 14.04).

All inputs of above models for MenShen have been included in MenShen tool.

 


©2017 SEG, Nanjing University