Eintrag kommentierenEintrag bewerten
Dieser Eintrag wurde im Schnitt mit 0 von 5 Punkten bewertet
Verification Result
Externe Quellen zum Thema NEU: Externe Quellen zum Thema suchen 
Beschreibung der Erfahrung
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
Externe Quellen zum Thema NEU: Externe Quellen zum Thema suchen 
 Eintrag kommentieren 
 Eintrag bewerten 
Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben.
Zum Seitenanfang Top Drucken Impressum AGB

VSEK ©2001-2018