Rodrigues18
Rodrigues et al. [1] performed a case study with the UPPAAL tool in 2018. They modelled a Body-Sensor-Network (BSN). To verify a set of requirements, they added an observer, which seems to be made by hand.
The models are available from the authors HERE.
Bodyhub
Timer
Generator
Module
Scheduler
Sensornode
Hand-made Observer
The requirements presented in the paper are listed in the following table:
Requirement
Whenever the scheduler cycle is completed, implies that the bodyhub and the three sensors have been executed
Approach
We broke this requirement down into two parts: first we handled the bodyhub (BSN-P01), then the sensors (BSN-P02). For both we used the Existence pattern, since the states idle in the bodyhub and sensors express that they have been executed. The scheduler cycle ends with the done property within the scheduler. We added a state to this automaton to observe it:
States DONE and IDLE can now be observed easily. They will be the Q and R for the scope we chose: Between Q and R.
To summarise, we chose the Existence pattern with the Between scope, since we can now observe every scheduler cycle, compared to the Precedence Pattern.
To observe the bodyhub (and the sensor) we only had to change the state's name idle to some unique name, we chose Idle for this.
Results
For the bodyhub part, the tool's runtime was 0.654s, UPPAAL's verification runtime was 77.279s. The consumed memory was 2.602308GB. 13 states and 16 transitions were added automatically. The property was satisfied.
For the sensornode part, the tool's runtime was 0.664s, UPPAAL's verification runtime was 101.433s. The consumed memory was 3.436476GB. 13 states and 16 transitions were added automatically. The property was satisfied.
Requirement
Whenever the patients’ health status is on high risk and an emergency has been detected it implies that the observer’s clock is less or equal 250 (ms) and a single scheduler cycle has elapsed since last data acquisition.
Approach
We broke this requirement down once again, first into a Bounded Existence-Between (BSN-P04), basically:
Between the bodyhub status is high and an emergency is detected, a new scheduler cycle must not be finished
We again had to modify the system model to express the variables high and emergency_detected as states:
Also, we modified the scheduler as described above for P 02.
This property now ensures that a new scheduler cycle cannot end until the emergency is detected, but to enforce that eventually an emergency will be detected, we used the Response-Globally pattern, with high being the request and emergency_detected being the response (BSN-P05).
Results
For the Bounded Existence part, the tool's runtime was 0.778s, UPPAAL's verification runtime was 92.911s. UPPAAL consumed 2.616812GB of memory. 15 states and 18 transitions were added automatically. The property was satisfied.
For the Response part, the tool's runtime was 0.617s, UPPAAL's verification runtime was 172.102s and the consumed memory was 1.983700GB. No states or transitions were added automatically. The property was satisfied.
Requirement
Whenever the sensornodes’ controller grants permission to execute and its on high risk, t_high schedulers’ cycle may have passed since the last data acquisition.
Approach
To observe the sensornodes, we made the following changes to the system model:
Basically, we are interested in the state ready in the sensornode when exe==true. We therefore added the state r_e and from that we are interested in the state where the sn_status == high, if this is the case, t == t_high must hold.
We therefore concluded to use the Response-Globally pattern here, Request and Response being the respective states for the property. Note, that this approach does not ensure that Response holds right after Request, but instead at some later point. We believe that t==t_high would not hold then. If our assumption is wrong, we should use the Existence-Between pattern, between a Request and collected, the Response should hold at some point.
Results
The tool's runtime was 0.761s, UPPAAL's verification runtime was 51.828s and the memory consumption was 1.295556GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since sensornode is a template that can be instantiated multiple times. We therefore changed sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whenever the sensornodes’ controller grants permission to execute and its on moderate risk, t _mod schedulers’ cycles may have passed since the last data acquisition.
Approach
We used the same approach as we did above in P 04. The just changed the variables from high to moderate or mod accordingly:
Similar to P 04, we made the same assumptions.
Results
The tool's runtime was 0.633s, UPPAAL's verification runtime was 50.122s and memory consumption was 1.296316GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since sensornode is a template that can be instantiated multiple times. We therefore changed sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whenever the sensornodes’ controller grants permission to execute and its on low risk, t _low schedulers’ cycles may have passed since the last data acquisition.
Approach
We used the same approach as we did above in P 04. The just changed the variables from high to low accordingly:
Similar to P 04, we made the same assumptions.
Results
The tool's runtime was 0.629s, UPPAAL's verification runtime was 52.436s and memory consumption was 1.296336GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since sensornode is a template that can be instantiated multiple times. We therefore changed sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whenever a sensor node has collected data, the bodyhub will eventually process it.
Approach
We were able to use the Response-Globally pattern here without any modifications.
Results
The tool's runtime was 0.623s, UPPAAL's verification runtime was 55.287s and memory consumption was 1.402040GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since bodyhub and sensornode are templates that can be instantiated multiple times. We therefore changed bodyhub to bodyhub(0) and sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whether the sensornode has collected some data, eventually the bodyhub will persist it.
Approach
We were able to use the Response-Globally pattern here without any modifications.
Results
The tool's runtime was 0.631s, UPPAAL's verification runtime was 55.3s and memory consumption was 1.410932GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since bodyhub and sensornode are templates that can be instantiated multiple times. We therefore changed bodyhub to bodyhub(0) and sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whenever a sensor node has sent data, the bodyhub will eventually process low, moderate or high data.
Approach
We were able to use the Response-Globally pattern here. We modified the system model to check for the variable bodyhub.received or bodyhub.received_data.
Results
The tool's runtime was 0.636s, UPPAAL's verification runtime was 57.836s and memory consumption was 1.401624GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since bodyhub and sensornode are templates that can be instantiated multiple times. We therefore changed bodyhub to bodyhub(0) and sensornode to sensornode(1) in the UPPAAL-query.
Requirement
Whether the bodyhub has processed some data, it eventually will detect a new patient health status.
Approach
We were able to use the Response-Globally pattern here without any modifications.
Results
The tool's runtime was 0.646s, UPPAAL's verification runtime was 54.103s and memory consumption was 1.400144GB. No states or transitions were added automatically. The property was satisfied.
Note, that we had to manually adapt the query since bodyhub is a template that can be instantiated multiple times. We therefore had to change bodyhub to bodyhub(0) in the UPPAAL-query.
[1]: Rodrigues, Arthur, et al. "A learning approach to enhance assurances for real-time self-adaptive systems." 2018 IEEE/ACM 13th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS). IEEE, 2018.