ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Ihre E-Mail wurde erfolgreich gesendet. Bitte prüfen Sie Ihren Maileingang.

Leider ist ein Fehler beim E-Mail-Versand aufgetreten. Bitte versuchen Sie es erneut.

Vorgang fortführen?

Exportieren
Filter
  • Weitere Quellen  (78)
  • 2015-2019  (78)
Sammlung
Datenquelle
Schlagwörter
Verlag/Herausgeber
Sprache
Erscheinungszeitraum
Jahr
  • 1
    facet.materialart.
    Unbekannt
    A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision (2018)
    In:  CASI
    Details
    Publikationsdatum: 2019-06-22
    Beschreibung: This paper presents a formally verified decision procedure for determining the satisfiability of a system of univariate polynomial relations over the real line. The procedure combines a root counting function, based on Sturm's theorem, with an interval subdivision algorithm. Given a system of polynomial relations over the same variable, the decision procedure progressively subdivides the real interval into smaller intervals. The subdivision continues until the satisfiability of the system can be determined on each subinterval using Sturm's theorem on a subset of the system's polynomials. The decision procedure has been formally verified in the Prototype Verification System (PVS). In PVS, the decision procedure is specified as a computable Boolean function on a deep embedding of polynomial relations. This function is used to define a proof producing strategy for automatically proving existential and universal statements on polynomial systems. The soundness of the strategy solely depends on the internal logic of PVS.
    Schlagwort(e): Numerical Analysis
    Materialart: NF1676L-28675 , Journal of Formalized Reasoning (e-ISSN 1972-5787); 11; 1; 19-41
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 2
    facet.materialart.
    Unbekannt
    A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (2018)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-20
    Beschreibung: The Automatic Dependent Surveillance-Broadcast (ADS-B) system allows aircraft to communicate their current state, including position and velocity information, to other aircraft in their vicinity and to ground stations. The Compact Position Reporting (CPR) algorithm is the ADS-B module responsible for the encoding and decoding of aircraft positions. CPR is highly sensitive to computer arithmetic since it heavily relies on functions that are intrinsically unstable such as floor and modulo. In this paper, a formally-verified double-precision floating-point implementation of the CPR algorithm is presented. The verification proceeds in three steps. First, an alternative version of CPR, which reduces the floating-point rounding error is proposed. Then, the Prototype Verification System (PVS) is used to formally prove that the ideal real-number counterpart of the improved algorithm is mathematically equivalent to the standard CPR definition. Finally, the static analyzer Frama-C is used to verify that the double-precision implementation of the improved algorithm is correct with respect to its operational requirement. The alternative algorithm is currently being considered for inclusion in the revised version of the ADS-B standards document as the reference implementation of the CPR algorithm.
    Schlagwort(e): Documentation and Information Science
    Materialart: NF1676L-29231 , International Symposium on Formal Methods; Jul 18, 2018 - Jul 17, 2018; Oxford; United Kingdom
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 3
    facet.materialart.
    Unbekannt
    Coordination Logic for Repulsive Resolution Maneuvers (2016)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: This paper presents an algorithm for determining the direction an aircraft should maneuver in the event of a potential conflict with another aircraft. The algorithm is implicitly coordinated, meaning that with perfectly reliable computations and information, it will in- dependently provide directional information that is guaranteed to be coordinated without any additional information exchange or direct communication. The logic is inspired by the logic of TCAS II, the airborne system designed to reduce the risk of mid-air collisions between aircraft. TCAS II provides pilots with only vertical resolution advice, while the proposed algorithm, using a similar logic, provides implicitly coordinated vertical and horizontal directional advice.
    Schlagwort(e): Air Transportation and Safety
    Materialart: NF1676L-22876 , AIAA Aviation 2016; Jun 13, 2016 - Jun 17, 2016; Washington, DC; United States
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 4
    facet.materialart.
    Unbekannt
    DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems (2015)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: 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.
    Schlagwort(e): Air Transportation and Safety
    Materialart: NF1676L-20901 , 2015 AIAA/IEEE Digital Avionics Systems Conference; Sep 13, 2015 - Sep 17, 2015; Prague; Czechoslovakia
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unbekannt
    Human-In-The-Loop Experimental Research for Detect and Avoid (2015)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: 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.
    Schlagwort(e): Air Transportation and Safety
    Materialart: NF1676L-20923 , 2015 IEEE/AIAA Digital Avionics Systems Conference (DASC); Sep 13, 2015 - Sep 17, 2015; Prague; Czechoslovakia
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unbekannt
    Detect and Avoid Alerting Logic for Unmanned Systems (2015)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: No abstract available
    Schlagwort(e): Air Transportation and Safety
    Materialart: NF1676L-21129 , UAS in the NAS Project Meeting; May 26, 2016; Hampton, VA; United States
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unbekannt
    Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems (2015)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: 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.
    Schlagwort(e): Air Transportation and Safety; Computer Programming and Software
    Materialart: NF1676L-22020 , International Colloquium on Theoretical Aspects of Computing (ICTAC 2015); Oct 29, 2015 - Oct 31, 2015; Cali; Colombia
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unbekannt
    Software Validation via Model Animation (2015)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: 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.
    Schlagwort(e): Computer Programming and Software
    Materialart: NF1676L-20845 , International Conference on Tests & Proofs (TAP 2015); Jul 22, 2015 - Jul 24, 2015; L''Aquila; Italy
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unbekannt
    Evolving Reliability and Maintainability Allocations for NASA Ground Systems (2016)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: This paper describes the methodology and value of modifying allocations to reliability and maintainability requirements for the NASA Ground Systems Development and Operations (GSDO) programs subsystems. As systems progressed through their design life cycle and hardware data became available, it became necessary to reexamine the previously derived allocations. This iterative process provided an opportunity for the reliability engineering team to reevaluate allocations as systems moved beyond their conceptual and preliminary design phases. These new allocations are based on updated designs and maintainability characteristics of the components. It was found that trade-offs in reliability and maintainability were essential to ensuring the integrity of the reliability and maintainability analysis. This paper discusses the results of reliability and maintainability reallocations made for the GSDO subsystems as the program nears the end of its design phase.
    Schlagwort(e): Quality Assurance and Reliability
    Materialart: KSC-E-DAA-TN30349 , IEEE Aerospace Conference; Mar 05, 2016 - Mar 12, 2016; Big Sky, MT; United States
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unbekannt
    Evolving Reliability and Maintainability Allocations for NASA Ground Systems (2016)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: This paper describes the methodology that was developed to allocate reliability and maintainability requirements for the NASA Ground Systems Development and Operations (GSDO) program's subsystems. As systems progressed through their design life cycle and hardware data became available, it became necessary to reexamine the previously derived allocations. Allocating is an iterative process; as systems moved beyond their conceptual and preliminary design phases this provided an opportunity for the reliability engineering team to reevaluate allocations based on updated designs and maintainability characteristics of the components. Trade-offs in reliability and maintainability were essential to ensuring the integrity of the reliability and maintainability analysis. This paper will discuss the value of modifying reliability and maintainability allocations made for the GSDO subsystems as the program nears the end of its design phase.
    Schlagwort(e): Quality Assurance and Reliability
    Materialart: KSC-E-DAA-TN27588 , IEEE Aerospace Conference; Mar 05, 2016 - Mar 12, 2016; Big Sky, MT; United States
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
Schließen ⊗
Diese Webseite nutzt Cookies und das Analyse-Tool Matomo. Weitere Informationen finden Sie hier...