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

quality98%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.