# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 7 Case Study: Temperature-Measuring System
* Data independence detection: We can suppose that the system's various \(SSR\)s will measure additional elements such as pressure and humidity. However, if there is no association between \(TMPRT\) and these additional variables, there is no need to include them in the system model. This definitely provides for a reduction in the complexity and size of the considered model. * Eliminating functional dependencies: Assume that the \(CLLTR\) saves the average of the readings received from the various \(SSR\)s. In this situation, it is evident that there is a direct relationship between the stored variable and the data measured by the \(SSR\)s. Thus, in order to simplify the complexity of the verification process, we must account for the connection between these various variables by removing the new variable corresponding to the average value because it can be determined from other variables. * Exploiting reversible rules: Consider the finite state machine that describes the behavior of \(SSR\) 1. This finite state machine can be simplified further by merging the two nodes connected by the transition \(Measure(Temp\ 1)\), as this operation can be viewed as internal and has no effect on the FV of the entire system. Similarly, we can compress the pairs of \(CLLTR\) finite state machine nodes connected by \(Store(Temp\ i)\) transitions. After verification, the collapsed nodes can be separated as they were originally. Second, we discuss MBT:
* Refinement techniques: This technique considers an untimed specification (\(Spec\)) and a set of refinement rules that allow each high-level untimed activity to be transformed into a sequence of low-level timed actions. Test cases (\(TSTCS\)s) are retrieved from the untimed \(Spec\) and refined into timed \(TSTCS\)s using the refinement procedures that have been established. For example, in Figure 8, the operation \(Measure(Temp\ 1)\) is refined into a sequence of four timed actions: \(TMPRT\) is measured by recording three successive values and then taking the average of these three values. This dramatically simplifies the test-creation technique and greatly decreases the calculation time and space requirements. Figure 8: A refinement of a high-level action. Figure 7: A simplification of the model considering symmetry aspects. * Reducing the size of digital-clock tests: A digital-clock test can be thought of as a particular tree with a special _Tick_ action, which mimics time progression. The purpose of this phase is to reduce the size of the test tree by compacting _Tick_ action sequences. This technique is presented in Figure 9, where a sequence of ten _Tick_ actions is replaced with just one transition labeled with 10 _Ticks_. The size of the exams is greatly decreased in this way. * Timed automaton (TA) tester generation: When the system \(Spec\) is presented as a non-deterministic timed automaton, there are two alternatives for test generation. The first option is to generate \(TSTCS\) on the fly. That is, test generation and test execution are carried out concurrently. This first option is challenging in general since it necessitates the use of high-performance calculators. The second option is to pre-determine the considered timed automaton before running the test. In Figure 10, for example, we suggest a non-deterministic version of a section of the model of the investigated system. This automaton is non-deterministic since the same action leads to different successor nodes from the beginning node. This non-determinism corresponds to the fact that the \(SSR\) may estimate \(TMPRT\) by computing the average of three collected data or only two values depending on some internal choices (for example, available resources). The result of the determinization of the non-deterministic automaton is shown in the same image. As previously stated, this method is not always practicable in a precise manner. As a result, we may need to make some assumptions. * \(TSTCS\) updating: As our system evolves, we must update the model accordingly.