Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMPP/MSAWseqPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 5 kB

Quelle atc.vdmpp Sprache: VDM

class AirTrafficController is subclass of GLOBAL

instance variables

radars    : set of Radar    := {};
obstacles : set of Obstacle := {};
history   : map FOId to (seq of Position) := {|->};

operations

public getDirectionVectors : FOId ==> seq of Vector
getDirectionVectors(id) ==
  let hist = history(id),
      p1 = hist(3),
      p2 = hist(2),
      p3 = hist(1)
  in
    return [mk_Vector(p1.coord.X - p2.coord.X,
                      p1.coord.Y - p2.coord.Y),
            mk_Vector(p2.coord.X - p3.coord.X,
                      p2.coord.Y - p3.coord.Y)]
pre id in set dom history and len history(id) = 3;

public getAltitudeHistory : FOId ==> seq of nat
getAltitudeHistory(id) ==
  let hist = history(id),
      lastHist = hist(1,...,2)
  in
    return [lastHist(i).altitude | i in set inds lastHist]
pre id in set dom history and len history(id) = 3;

public updateHistory : () ==> ()
updateHistory() ==
(
   cleanUpHistory();
   for all r in set radars
   do
    (for all fo in set r.getDetected()
     do
      registerHistory(fo);
    )
);

private registerHistory : FO ==> ()
registerHistory(fo) ==
(let id = fo.getId(),
      coor = fo.getCoordinates(),
      alt = fo.getAltitude()
  in
    if id in set dom history
    then history := history ++
                    {id |-> addHistory(history(id),coor,alt)}
    else history := history munion
                    {id |-> addHistory([],coor,alt)}
);

public cleanUpHistory : () ==> ()
cleanUpHistory() ==
(let alldetected = dunion {r.getDetected() | r in set radars},
      allids = { fo.getId() | fo in set alldetected }
  in
    history := allids <: history
);

functions
private addHistory : History * Coordinates * Altitude  -> History
addHistory(hist,coord,alt) ==
  if(len hist < 3)
  then hist ^ [mk_Position(coord,alt)]
  else tl hist ^ [mk_Position(coord,alt)];

operations

public addRadar : Radar ==> ()
addRadar(r) ==
  radars := {r} union radars;

public addObstacle : Obstacle ==> ()
addObstacle(ob) ==
  obstacles := {ob} union obstacles;

public findThreats : () ==> ()
findThreats() ==
  let allFOs = dunion { r.getDetected() | r in set radars }
  in
   (for all fo in set allFOs
    do
      for all ob in set obstacles
      do
        if not isFOSafe(ob,fo.getPosition())
        then writeObjectWarning(ob,fo)
        else
          if len history(fo.getId()) = 3
          then willFObeSafe(ob,fo);
    for all r in set radars
    do
      if r.saturatedRadar()
      then writeRadarWarning(r)
   );

public detectedByTwoRadars : set of Radar ==> set of FO
detectedByTwoRadars(r) ==
  return dunion {a.getDetected() inter b.getDetected()
                 | a,b in set r & a <> b};

public detectedByAllRadars : set of Radar ==> set of FO
detectedByAllRadars(r) ==
  return dinter {rad.getDetected() | rad in set r};

public Step : () ==> ()
Step() ==
( for all r in set radars
  do
    r.Scan(MSAW`airspace);
  updateHistory();
  findThreats();
);

functions

isFOatSafeAltitude : MinimumSafetyAltitude * Position -> bool
isFOatSafeAltitude(msa,pos) ==
  msa <> <NotAllowed> and msa < pos.altitude;

operations

isFOSafe : Obstacle * Position ==> bool
isFOSafe(obs,pos) ==
  let obsloc      = obs.getCoordinates(),
      secureRange = obs.getSecureRange(),
      foloc       = pos.coord
  in
    if isPointInRange(obsloc,secureRange,foloc)
    then isFOatSafeAltitude(obs.getMSA(),pos)
    else return false;

willFObeSafe : Obstacle * FO ==> ()
willFObeSafe(obs,fo) ==
  let pred = isPredictPossible(fo)
  in
    for all p in set pred
    do
      if not isFOSafe(obs,p)
      then
        let id   = fo.getId(),
            cs   = fo.getCoordinates(),
            alt  = fo.getAltitude(),
            type = <EstimationWarning>,
            msa  = obs.getMSA(),
            t    = World`timerRef.GetTime()
        in
         (World`env.handleFOWarningEvent(id, cs, alt, type, msa, t);
          return
         )
pre fo.getId() in set dom history and  len history(fo.getId()) = 3;


private writeObjectWarning : Obstacle * FO ==> ()
writeObjectWarning(obs,fo) ==
  let id   = fo.getId(),
      cs   = fo.getCoordinates(),
      alt  = fo.getAltitude(),
      type = obs.getType(),
      msa  = obs.getMSA(),
      t    = World`timerRef.GetTime()
  in
    World`env.handleFOWarningEvent(id, cs, alt, type, msa, t);

private writeRadarWarning : Radar ==> ()
writeRadarWarning(r) ==
  let coord   = r.getLocation(),
      range   = r.getRange(),
      radWarn = <Saturated>,
      num     = card r.getDetected(),
      t       = World`timerRef.GetTime()
  in
    World`env.handleRadarWarningEvent(coord,range,radWarn,num,t);


private isPredictPossible : FO ==> [set of Position]
isPredictPossible(fo)==
  let hist = history(fo.getId())
  in
    if len hist < 3
    then return nil
    else return predictPosition(fo)
pre fo.getId() in set dom history ;


private predictPosition : FO ==> set of Position
predictPosition(fo) ==
  let foid   = fo.getId(),
      vs     = getDirectionVectors(foid),
      estVec = vectorRotate(vs(1),signedVectorAngle(vs(2),vs(1))),
      estAlt = predictAltitude(getAltitudeHistory(foid)),
      estCoo = addVectorToPoint(estVec,history(foid)(3)),
      estPos = mk_Position(estCoo,estAlt)

  in
    return calculateNeighborhood(estPos)
pre fo.getId() in set dom history and len history(fo.getId()) = 3;

functions
private calculateNeighborhood : Position -> set of Position
calculateNeighborhood(pos) ==
{pos,
  mk_Position(addVectorToPoint(mk_Vector(2,0),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(-2,0),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(0,2),pos),pos.altitude),
  mk_Position(addVectorToPoint(mk_Vector(0,-2),pos),pos.altitude)
};

private predictAltitude : seq of nat -> nat
predictAltitude(alts) ==
  alts(1) + (alts(1) - alts(2))
pre len alts = 2;

end AirTrafficController

quality85%

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