Quelle vertical_los_crit_CA.pvs Sprache: PVS

%------------------------------------------------------------------------------
%    Loss of Separation Criterion: Vertical
%
%    This criterion allows for a backup system that performs
%    Collision Avoidance in the Event of A Near Collision (E.g. TCAS).
%    The collision avoidance system is assumed to activate when a cylinder
%    around the intruder of radius caD and height caH is expected to be
%    entered by the ownship within time caTime.
%------------------------------------------------------------------------------
vertical_los_crit_CA[D,H,caD,caH,caTime: posreal,
         ( IMPORTING definitions_3D )
         break_vz_symm:[Vect3 ->  Sign] %% Break symmetry when v`z = 0
      ] : THEORY
BEGIN

  ASSUMING

    break_vz_symm_comm : ASSUMPTION
      FORALL (s:Vect3):
        s /= zero IMPLIES
        break_vz_symm(-s) = -break_vz_symm(s)

    break_vz_symm_sz : ASSUMPTION
      FORALL (s:Vect3):
        s`z /= 0 IMPLIES
        break_vz_symm(s) = sign(s`z)

    % Future work: continuity of break symmetry

  ENDASSUMING

  IMPORTING vertical_los_criterion[D,H],
     cd3d[caD,caH,0,caTime],
     cd3d_ever[caD,caH]

  vo,vi,
  nvi,nvo,
  v,nv    : VAR Vect3
  s : VAR Vect3
  t,t1,t2,
  tm      : VAR real
  tr      : VAR posreal %% Parameter that specifies maximum time to recover
  eps   : VAR Sign
  tn   : VAR nnreal
  sz,vz,
  nvz,
  voz,viz,
  nvoz,
  nviz,
  soz,siz    : VAR real
  MinRelVertSpeed,
  MinRelVertSpeedo,
  MinRelVertSpeedi: VAR posreal

  %%% This file implements a specific element of the type EpsChooser,
  %%% which is defined in vertical_los_generic. It then constructs the
  %%% associated criterion with the function vertical_los_crit_epschooser?
  %%% that is defined in that file.

  %%% Recall from vertical_los_generic that EpsChooser picks an epsilon
  %%% (-1 or 1) (up or down). A decision vector is a function that takes
  %%% s, vo, and vi and returns another vector on which the decision
  %%% of epsilon will be made.

  Decision_Vector : TYPE+ = {f:[[Vect3,Vect3]->Vect3]| FORALL (s,v):
    (s /= zero OR v/=zero) => (f(s,v)/=zero AND f(-s,-v)=-f(s,v))}

  dv: VAR Decision_Vector

  dv_to_ec(dv)(s,v): Sign =
    break_vz_symm(dv(s,v))

  dv_to_ec_antisymmetric: JUDGEMENT
    dv_to_ec(dv) HAS_TYPE Vertical_Strategy[D,H]

  %%% The interior cylinder where CA applies:

  CA_applies?(s,v): bool = cd3d?[caD,caH,0,caTime](s,v)

  CA_cyl_conflict_ever?(s,v): bool =
    cd3d_ever?[caD,caH](s,v)

  %%% A specific decision vector for the new criterion:

  vertical_decision_vect(s,v): {vq: Vect3 | (s /= zero OR v/=zero) IMPLIES vq/=zero} =
    IF (s/=zero AND CA_cyl_conflict_ever?(s,v)) OR (s/=zero AND v`z=0) THEN
       (IF s`z /= 0 OR sqv(v)=0 THEN s ELSE v ENDIF)
    ELSIF vect2(v) = zero OR s = zero THEN
       v
    ELSIF vect2(s)*vect2(v) <= 0 THEN
       s + horizontal_tca(s,v)*v
    ELSE
       s
    ENDIF

  vertical_decision_vect_antisymmetric: JUDGEMENT
    vertical_decision_vect HAS_TYPE Decision_Vector

  %%% The new criterion:

  vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) : bool =
    vertical_los_criterion?(s,v,dv_to_ec(vertical_decision_vect)(s,v),MinRelVertSpeed)(nv)

  % It is coordinated:

  vertical_los_crit_CA_independent: LEMMA
    LET eps: Sign = dv_to_ec(vertical_decision_vect)(s, v)
    IN
        s/=zero AND
vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) AND
vect2(s)*vect2(v) < 0 AND vect2(s)*vect2(nv) < 0 AND
norm(vect2(s+horizontal_tca(s,nv)*nv)) <= norm(vect2(s+horizontal_tca(s,v)*(v)))
IMPLIES
eps*(s+horizontal_tca((s),nv)*nv)`z >= eps*(s+horizontal_tca((s),v)*(v))`z

  vertical_los_crit_CA_independent_strong: LEMMA
     s/=zero AND
vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv) AND
vect2(s)*vect2(v) < 0 AND vect2(s)*vect2(nv) < 0 AND
norm(vect2(s+horizontal_tca(s,nv)*nv)) <= norm(vect2(s+horizontal_tca(s,v)*(v)))
IMPLIES
((v`z=0 OR CA_cyl_conflict_ever?(s,v)) AND
   sign(s`z)/=sign(v`z) AND abs((s+horizontal_tca((s),nv)*nv)`z) >= abs(s`z))
OR
abs((s+horizontal_tca((s),nv)*nv)`z) >= abs((s+horizontal_tca((s),v)*(v))`z)

  vertical_los_crit_CA_independent_vspeed: LEMMA
    s/=zero AND
      vertical_los_crit_CA?(s,v,MinRelVertSpeed)(nv)
      IMPLIES
      break_vz_symm(vertical_decision_vect(s,v))*(nv`z)>=MinRelVertSpeed

  vertical_los_crit_CA_coordinated_vspeed: LEMMA
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo)
      IMPLIES
      break_vz_symm(vertical_decision_vect(s,vo-vi))*(nvo`z-nvi`z)>=max(MinRelVertSpeedo,MinRelVertSpeedi)

  vertical_los_crit_CA_coordinated: LEMMA
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo)
      IMPLIES
      vertical_los_crit_CA?(s,vo-vi,max(MinRelVertSpeedo,MinRelVertSpeedi))(nvo-nvi)

  vertical_los_crit_CA_coordinated_strong: LEMMA
      LET v = vo-vi, nv = nvo-nvi IN
      s/=zero AND
      vertical_los_crit_CA?(s,vo-vi,MinRelVertSpeedo)(nvo-vi) AND
      vertical_los_crit_CA?(-s,vi-vo,MinRelVertSpeedi)(nvi-vo) AND
      vect2(s)*vect2(v) < 0
      IMPLIES
      vect2(s)*vect2(nv) >= 0 OR
      norm(vect2(s+horizontal_tca(s,nv)*nv)) > norm(vect2(s+horizontal_tca(s,v)*(v))) OR
      ((v`z=0 OR CA_cyl_conflict_ever?(s,v)) AND
         sign(s`z)/=sign(v`z) AND abs((s+horizontal_tca((s),nv)*nv)`z) >= abs(s`z)) OR
      abs((s+horizontal_tca((s),nv)*nv)`z) >= abs((s+horizontal_tca((s),v)*(v))`z)

END vertical_los_crit_CA

quality94%

¤ Dauer der Verarbeitung: 0.25 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.