# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 3 Preliminaries
### Model Checking  
Model checking is a rigorous verification method that presents a mathematical proof for a given property of the system. It accepts a system model and properties that the system model should satisfies. During verification, model checking explores all states of the system by taking every symbolic computational step and exhaustively check if every state satisfies given properties. Since model checking explores thoroughly all states of the system, it requires numerous time and memories. It is used to obtain guarantee of given properties of safety critical systems by mathematical proving techniques. In this paper, we apply UPPAAL, a model checker, to prove MAuth-CAN's properties. UPPAAL tool suite includes various analysis techniques such as symbolic model checking, statistical model checking, and simulation. Symbolic model checking of UPPAAL accepts timed automata (TA) [24] as modeling language and use CTL (Computational Tree Logic) for property specification. CTL in UPPAAL comprises path formulas and state formulas. A path formula consists of branch quantifiers and path quantifiers. \(A\) and \(E\), branch quantifiers, denotes \"all paths\" and \"any path\", respectively. \(\square\) and \(\diamondsuit\), path quantifiers, represent \"all states\" and \"exist a state\", respectively. Let \(\phi\) a state formula. A path formula along with a state formula is expressed by the grammar:  
\[\varphi::=\phi\mid A\square\phi\mid E\square\phi\mid A\diamondsuit\phi\mid E \diamondsuit\phi\mid\phi_{1}\rightarrow\phi_{2}\]  
Using such a formula, reachability, safety and liveness properties can be formulated in UPPAAL. Reachability properties are expressed by the path formula \(E\diamondsuit\phi\), meaning that a state satisfying \(\phi\) is reachable. Safety properties are formulated by the path formula \(A\square\). For example, \(A\square\phi\) requires that \(\phi\) should be true in all reachable states. Meanwhile, \(E\square\phi\) denotes that there exists a maximal path such that \(\phi\) is always true. A maximal path is a path that is either infinite or where the last state has no outgoing transitions [25]. Liveness properties are formulated by the path formula \(A\diamondsuit\phi\), which means that there exists a state satisfying \(\phi\) in all the branches, i.e., \(\phi\) is eventually satisfied. One of useful formulas is the leads to or response property, which are written \(A\square(\phi\rightarrow A\diamondsuit\psi)\). That means that whenever \(\phi\) happens, \(\psi\) should hold eventually [25]. For instance, whenever a message is sent, that should always be acknowledged. UPPAAL SMC accepts a network of stochastic timed automata (NSTA). A model of network of timed automata in UPPAAL is redefined by a network of stochastic timed automata where the non-determinism of behavior in a timed automata model is refined by a probability distribution, so that the property for a given model is characterized by a probability that an event happens or a property holds. The specification of UPPAAL SMC is based on Metric Interval Temporal Logic [26]. For an NSTA \(M\), \(\mathrm{P}_{M}\) (\(\left|\phi\right\rangle\) denotes the probability that a random run of \(M\) satisfies \(\phi\). The problem of checking \(\mathrm{P}_{M}\left(\phi\right)\geq p\) (\(p\in[0,1]\)) is undecidable. For this reason, for the sub-logic of cost-bounded reachability problem \(\mathrm{P}_{M}(\diamondsuit_{(x\leq C)}AP)\geq p\), where \(x\) is a clock, \(C\) is a time bound, and \(AP\) is a conjunction of predicates over the state of a NSTA, UPPAAL SMC approximates the answer using simulation-based algorithms [27]. In UPPAAL SMC, the following three types of questions can be answered:  
1. Probability estimation: What is the probability \(\mathrm{P}_{M}(\diamondsuit_{(x\leq C)}AP)\) for a given \(M\)? 2. Hypothesis testing: Is the probability \(\mathrm{P}_{M}(\diamondsuit_{(x\leq C)}AP)\) for a given \(M\) greater or equal to \(p\) [0, 1]? 3.