ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    facet.materialart.
    Unknown
    DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: This paper presents DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems), a reference implementation of a detect and avoid concept intended to support the integration of Unmanned Aircraft Systems into civil airspace. DAIDALUS consists of self-separation and alerting algorithms that provide situational awareness to UAS remote pilots. These algorithms have been formally specified in a mathematical notation and verified for correctness in an interactive theorem prover. The software implementation has been verified against the formal models and validated against multiple stressing cases jointly developed by the US Air Force Research Laboratory, MIT Lincoln Laboratory, and NASA. The DAIDALUS reference implementation is currently under consideration for inclusion in the appendices to the Minimum Operational Performance Standards for Unmanned Aircraft Systems presently being developed by RTCA Special Committee 228.
    Keywords: Air Transportation and Safety
    Type: NF1676L-20901 , 2015 AIAA/IEEE Digital Avionics Systems Conference; Sep 13, 2015 - Sep 17, 2015; Prague; Czechoslovakia
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 2
    facet.materialart.
    Unknown
    Human-In-The-Loop Experimental Research for Detect and Avoid (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: This paper describes a Detect and Avoid (DAA) concept for integration of UAS into the NAS developed by the National Aeronautics and Space Administration (NASA) and provides results from recent human-in-the-loop experiments performed to investigate interoperability and acceptability issues associated with these vehicles and operations. The series of experiments was designed to incrementally assess critical elements of the new concept and the enabling technologies that will be required.
    Keywords: Air Transportation and Safety
    Type: NF1676L-20923 , 2015 IEEE/AIAA Digital Avionics Systems Conference (DASC); Sep 13, 2015 - Sep 17, 2015; Prague; Czechoslovakia
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 3
    facet.materialart.
    Unknown
    Detect and Avoid Alerting Logic for Unmanned Systems (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: No abstract available
    Keywords: Air Transportation and Safety
    Type: NF1676L-21129 , UAS in the NAS Project Meeting; May 26, 2016; Hampton, VA; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 4
    facet.materialart.
    Unknown
    Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: As the technological and operational capabilities of unmanned aircraft systems (UAS) continue to grow, so too does the need to introduce these systems into civil airspace. Unmanned Aircraft Systems Integration in the National Airspace System is a NASA research project that addresses the integration of civil UAS into non-segregated airspace operations. One of the major challenges of this integration is the lack of an onboard pilot to comply with the legal requirement that pilots see and avoid other aircraft. The need to provide an equivalent to this requirement for UAS has motivated the development of a detect and avoid (DAA) capability to provide the appropriate situational awareness and maneuver guidance in avoiding and remaining well clear of traffic aircraft. Formal methods has played a fundamental role in the development of this capability. This talk reports on the formal methods work conducted under NASA's Safe Autonomous System Operations project in support of the development of DAA for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations. The talk also discusses technical challenges in formal methods research in the context of the development and safety analysis of advanced air traffic management concepts.
    Keywords: Air Transportation and Safety; Computer Programming and Software
    Type: NF1676L-22020 , International Colloquium on Theoretical Aspects of Computing (ICTAC 2015); Oct 29, 2015 - Oct 31, 2015; Cali; Colombia
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unknown
    Software Validation via Model Animation (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: This paper explores a new approach to validating software implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input values to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illustrated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system's algorithms are carried out in the Prototype Verification System (PVS). The animation tool PVSio is used to evaluate the formal models on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual software. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.
    Keywords: Computer Programming and Software
    Type: NF1676L-20845 , International Conference on Tests & Proofs (TAP 2015); Jul 22, 2015 - Jul 24, 2015; L''Aquila; Italy
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unknown
    Characterizing the Effects of a Vertical Time Threshold for a Class of Well-Clear Definitions (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: A fundamental requirement for the integration of unmanned aircraft into civil airspace is the capability of aircraft to remain well clear of each other and avoid collisions. This requirement has led to a broad recognition of the need for an unambiguous, formal definition of well clear. It is further recognized that any such definition must be interoperable with existing airborne collision avoidance systems (ACAS). A particular class of well-clear definitions uses logic checks of independent distance thresholds as well as independent time thresholds in the vertical and horizontal dimensions to determine if a well-clear violation is predicted to occur within a given time interval. Existing ACAS systems also use independent distance thresholds, however a common time threshold is used for the vertical and horizontal logic checks. The main contribution of this paper is the characterization of the effects of the decoupled vertical time threshold on a well-clear definition in terms of (1) time to well-clear violation, and (2) interoperability with existing ACAS. The paper provides governing equations for both metrics and includes simulation results to illustrate the relationships. In this paper, interoperability implies that the time of well-clear violation is strictly less than the time a resolution advisory is issued by ACAS. The encounter geometries under consideration in this paper are initially well clear and consist of constant-velocity trajectories resulting in near-mid-air collisions.
    Keywords: Air Transportation and Safety
    Type: NF1676L-20526
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unknown
    NASA Controller Acceptability Study 1(CAS-1) Experiment Description and Initial Observations (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: This paper describes the Controller Acceptability Study 1 (CAS-1) experiment that was conducted by NASA Langley Research Center personnel from January through March 2014 and presents partial CAS-1 results. CAS-1 employed 14 air traffic controller volunteers as research subjects to assess the viability of simulated future unmanned aircraft systems (UAS) operating alongside manned aircraft in moderate-density, moderate-complexity Class E airspace. These simulated UAS were equipped with a prototype pilot-in-the-loop (PITL) Detect and Avoid (DAA) system, specifically the Self-Separation (SS) function of such a system based on Stratway+ software to replace the see-and-avoid capabilities of manned aircraft pilots. A quantitative CAS-1 objective was to determine horizontal miss distance (HMD) values for SS encounters that were most acceptable to air traffic controllers, specifically HMD values that were assessed as neither unsafely small nor disruptively large. HMD values between 0.5 and 3.0 nautical miles (nmi) were assessed for a wide array of encounter geometries between UAS and manned aircraft. The paper includes brief introductory material about DAA systems and their SS functions, followed by descriptions of the CAS-1 simulation environment, prototype PITL SS capability, and experiment design, and concludes with presentation and discussion of partial CAS-1 data and results.
    Keywords: Air Transportation and Safety
    Type: NASA/TM-2015-218763 , L-20548 , NF1676L-20983
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unknown
    Kodiak: An Implementation Framework for Branch and Bound Algorithms (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: Recursive branch and bound algorithms are often used to refine and isolate solutions to several classes of global optimization problems. A rigorous computation framework for the solution of systems of equations and inequalities involving nonlinear real arithmetic over hyper-rectangular variable and parameter domains is presented. It is derived from a generic branch and bound algorithm that has been formally verified, and utilizes self-validating enclosure methods, namely interval arithmetic and, for polynomials and rational functions, Bernstein expansion. Since bounds computed by these enclosure methods are sound, this approach may be used reliably in software verification tools. Advantage is taken of the partial derivatives of the constraint functions involved in the system, firstly to reduce the branching factor by the use of bisection heuristics and secondly to permit the computation of bifurcation sets for systems of ordinary differential equations. The associated software development, Kodiak, is presented, along with examples of three different branch and bound problem types it implements.
    Keywords: Numerical Analysis
    Type: NASA/TM-2015-218776 , L-20559 , NF1676L-21365
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unknown
    DAIDALUS: Detect & Avoid Alerting Logic for Unmanned Systems (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: No abstract available
    Keywords: Air Transportation and Safety
    Type: NF1676L-21374 , Dagstuhl Seminar: Qualification of FM Tools; Apr 26, 2015 - Apr 29, 2015; Saarbrucken; Germany
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unknown
    Criteria Approach to Separation Assurance (2015)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: No abstract available
    Keywords: Air Transportation and Safety
    Type: NF1676L-21125 , 20150327_Boeing_Australia_Breifing; Mar 27, 2015; Hampton, VA; United States
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...