Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: integration_fault_model.pvs Sprache: PVS

Original von: 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.7 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.