| Applying UVE to the finally obtained abstract model yields that the requirement on the voting algorithm as formalised in Fig. "Formalisation" doesn't hold. The counter-example reveals the following non-obvious issue. Consider three sensors s1; s2; s3 with values s.t. the distance between the value of s2 and the values of s1 and s3 is smaller than the tolerance,
d(v(s1), v(s2)) ≤ δ,d(v(s2), v(s3)) ≤ δ,
but s1 deviates from s3 by more than the tolerance,
d(v(s1), v(s3)) > δ.
By the first two inequations, all sensors are voted correct. Now if s2 has failed in the past and is currently considered to be out of order, then only s1 and s3 contribute to the arithmetic average. And both have a distance larger than δ/2 from the arithmetic average. This violates the requirement stated in unit Treating Complexity by Abstraction I.
To Verification Runtimes
Back to overview Formal Verification of a Sensor Voting and Monitoring UML Model