## 5 Case Study
### Models and Verification of System Properties  
In this section, we first give the verification without time requirements, such as the deadlock checking and the checking with Linear Temporal Logic (LTL). Next, we model some properties with time requirements based on proposed property patterns and verify them with our algorithm embedded in the tool PAT.  
The verification results of deadlock and LTL checking are shown as follows:  
* The verification results of the assertions #_assert System deadlockfree_ and #_assert SystemWithAttacker deadlockfree_ are both true (through 184 states and 230 transitions and 91,146 states and 178,546 transitions, respectively), indicating that the deadlocks never occur in _System_ and _SystemWithAttacker_.
* The verification result of the assertion #_assert System \(|\)=\(|\)\(|\)\((\)\)\((\)\  
and 230 transitions), indicating that when the Sensor receives the message _WLToSen_ sent from the Heater, it can send the message _WLToCtrl_ to the Controller in one time unit. If the clock constraint \(x\leq 1\) is changed to \(x<1\), the verification result is false. The above verification with LTL (_#assert System |=I_)(_WLToSen_-\(><>\)_WLToCtrl_)) gives the result that the event _WLToCtrl_ always happens after _WLToSen_. This verification further shows that the event _WLToCtrl_ always happens after _WLToSen_ in one time unit.
* The property _Pre_ is modeled based on the property pattern _Precedence_-2. In Figure 9, we set the attack interval to be at least five time units and the detecting interval of the CtrlWithCon to be six time units. As the CtrlWithCon shown in Figure 9, if the conditions \(H>SH\) or \(L<SL\) are met, the Configuration will receive a message from CtrlWithCon to obtain the correct values of \(H\) and \(L\) and reply with the event _CorrectHL_. The property _Pre_ verifies whether the controller could receive the messages with correct values of \(H\) and \(L\), after the Attacker sends error messages, i.e., the event _FalseHL_. _FalseHL_ can occur many times before CtrlWithCon notices it (i.e., the event _ObtainHL_), because the attacker can launch the attacks continuously (see the self-transition on the state Recover). The clock \(x\) is sticking after the first occurrence of _FalseHL_. The assertion is: _#assert SystemWithAttacker refines_\(<\)\(T\)\(>\)_Pre_. The verification result is true (through 36,094 states and 71,836). If the number in the clock constraint \(x\leq 7\) is changed to a smaller one, then the verification result is false. This means that the system is able to recover within seven time units after being attacked. The above verification with LTL (_#assert SystemWithAttacker|=I_)(_FalseHL_-\(><>\)_CorrectHL_)) gives the result that the event _CorrectHL_ always happens after the event _FalseHL_. This verification further shows that the event _CorrectHL_ always happens after the event _FalseHL_ in seven time units.
* The property _Existence_ is modeled based on the property pattern _Existence-1_. The assertion is: _#assert SystemWithAttacker refines_\(<\)\(T\)\(>\)_Existence_. The verification result of the property _Existence_ is true (through 33,889 states and 67,375 transitions). This means that the system is able to examine whether the system is under attack within six time units, which shows that the system can automatically recover after being attacked. The above verification with LTL (_#assert SystemWithAttacker |=I_)\(<\)\(>\)_ObtainHL_) gives the result that the event _ObtainHL_ can always happen if the attacker exists. This verification further shows that the time between two successive occurrences of the event _ObtainHL_ is at most six time units.