## 2 Models for SOFC and their Verification Degree
### A Short Overview of Methods with Result Verification  
Methods with result verification, for example, interval arithmetic [8], affine arithmetic [18], or Taylor models [19], are constructed in such a way as to mathematically ensure a priori that the results produced by their implementation on a computer will be correct. An important effect of this view is that such methods allow us to take into account bounded uncertainty in parameters explicitly. Figure 1: Schematic visualization of the thermal subsystem of the SOFC stack with preheaters. Note that this does not include making sure that the _code_ of the implementation is correct, which is the subject matter of code verification [20; 21]. As a simple example of a method with result verification, consider obtaining a verified result of the sum \(a+b\) with the help of interval analysis, where \(a,b\in\mathbf{R}\) are not representable as floating point numbers. First, it is necessary to compute representations of these numbers as intervals (i.e., their _enclosures_) \([a]=[\underline{a},\overline{a}]\) and \([b]=[\underline{b},\overline{b}]\) with floating point bounds \(\underline{a},\,\underline{b},\,\overline{a},\,\overline{b}\), which is usually done by directed rounding. The lower bound is the largest representable number smaller than the exact one (rounding down, to \(-\infty\), denoted by \(\
abla\)). The upper bound is the smallest floating point number greater than the considered one (rounding up, to \(+\infty\), \(\triangle\)). The details on rigorous implementation possibilities for this procedure, even in the case when the IEEE 754 roundings to \(\pm\infty\) are not available, are given in [22]. The sum is then enclosed according to the rule \([a]+[b]=\{a+b\}\) for all \(a\in[a]\), \(b\in[b]\}=[\underline{a}+\underline{b},\overline{a}+\overline{b}]\), where the lower bound \(\underline{s}=\underline{a}+\underline{b}\) has to be rounded down if it is not representable in the floating point arithmetic used on a computer, and the upper bound \(\overline{s}=\overline{a}+\overline{b}\) is rounded up. In this way, the true result \(s=a+b\) of the addition is always inside the interval \([\
abla\underline{s},\triangle\overline{s}]\) obtained using a computer, and all rounding or conversion errors are taken care of. Such rules can be devised for all basic arithmetic operations and elementary functions. They need not necessarily rely on intervals, but can take internal dependencies of variables into account, for example, in a linear way as in affine arithmetic or as a polynomial of a higher degree as in Taylor model arithmetic. To prove the correctness of results for more advanced algorithms such as those for solving algebraic or differential equations, fixed point theorems are employed. There are a number of software libraries for methods with result verification which implement the corresponding arithmetics (e.g, C-XSC [23] for intervals) and higher level algorithms (e.g., VNODE-LP [24] for solving initial value problems with the help of interval analysis). As already mentioned in the introduction, the main disadvantage of methods with result verification is the possibility of too conservative bounds (e.g., \(\pm\infty\)) which appear because of the dependency problem or wrapping effect (the latter being a variation of the former). As a simple example, consider the difference of the interval \([\underline{a},\overline{a}]=\{x\in\mathbf{R}\mid\underline{a}\leq x\leq \overline{a},\,\underline{a}<\overline{a}\,\,\}\) and itself: \([\underline{a},\overline{a}]-[\underline{a},\overline{a}]=[\underline{a}, \overline{a}]+[-\overline{a},-\underline{a}]\). According to the general definition, the true result (which is zero) is inside the interval \([\underline{a}-\overline{a},\overline{a}-\underline{a}]\) of the nonzero width \(2(\overline{a}-\underline{a})\), which contains zero, but is not equal to it. In addition, the width of the resulting enclosure is twice the width of the interval \([\underline{a},\overline{a}]\) (which is equal to \(\overline{a}-\underline{a}\)).