| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle integration_fault_model.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose : integration fault model with mapping to the % results-based fault model. % % integration_fault_model[N:posnat]: THEORY BEGIN IMPORTING finite_sets_below_extra[N] p : VAR below(N) % the fault types for the integration fault model fault_class: TYPE = {good, omissive_symmetric, omissive_asymmetric, transmissive_symmetric, single_error_asymmetric, transmissive_asymmetric} fcl : var fault_class correct_denotation?(fcl) : bool = good?(fcl) OR omissive_symmetric?(fcl) OR omissive_asymmetric?(fcl) symmetric_denotation?(fcl) : bool = good?(fcl) OR omissive_symmetric?(fcl) OR transmissive_symmetric?(fcl) single_denotation?(fcl) : bool = NOT transmissive_asymmetric?(fcl) node_status: TYPE = [below(N) -> fault_class] status: VAR node_status good(status) : finite_set[below(N)] = {p | good?(status(p))} omissive_symmetric(status) : finite_set[below(N)] = {p | omissive_symmetric?(status(p))} omissive_asymmetric(status) : finite_set[below(N)] = {p | omissive_asymmetric?(status(p))} transmissive_symmetric(status) : finite_set[below(N)] = {p | transmissive_symmetric?(status(p))} single_error_asymmetric(status) : finite_set[below(N)] = {p | single_error_asymmetric?(status(p))} transmissive_asymmetric(status) : finite_set[below(N)] = {p | transmissive_asymmetric?(status(p))} correct_denotation(status) : finite_set[below(N)] = {p | correct_denotation?(status(p))} symmetric_denotation(status): finite_set[below(N)] = {p | symmetric_denotation?(status(p))} single_denotation(status): finite_set[below(N)] = {p | single_denotation?(status(p))} symmetric_single_denotation: LEMMA subset?(symmetric_denotation(status), single_denotation(status)) END integration_fault_model ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28