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
  • Computer Programming and Software  (10)
  • 2020-2024
  • 2020-2021
  • 2005-2009  (10)
Sammlung
Schlagwörter
Erscheinungszeitraum
Jahr
  • 1
    facet.materialart.
    Unbekannt
    From Verified Models to Verifiable Code (2009)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: Declarative specifications of digital systems often contain parts that can be automatically translated into executable code. Automated code generation may reduce or eliminate the kinds of errors typically introduced through manual code writing. For this approach to be effective, the generated code should be reasonably efficient and, more importantly, verifiable. This paper presents a prototype code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into an intermediate language and subsequently to multiple target programming languages. Several case studies are presented to illustrate the tool's functionality. The generated code can be analyzed by software verification tools such as verification condition generators, static analyzers, and software model-checkers to increase the confidence that the generated code is correct.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2009-215943 , L-19766 , LF99-9439
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 2
    facet.materialart.
    Unbekannt
    Experimental Evaluation of a Planning Language Suitable for Formal Verification (2008)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: The marriage of model checking and planning faces two seemingly diverging alternatives: the need for a planning language expressive enough to capture the complexity of real-life applications, as opposed to a language simple, yet robust enough to be amenable to exhaustive verification and validation techniques. In an attempt to reconcile these differences, we have designed an abstract plan description language, ANMLite, inspired from the Action Notation Modeling Language (ANML) [17]. We present the basic concepts of the ANMLite language as well as an automatic translator from ANMLite to the model checker SAL (Symbolic Analysis Laboratory) [7]. We discuss various aspects of specifying a plan in terms of constraints and explore the implications of choosing a robust logic behind the specification of constraints, rather than simply propose a new planning language. Additionally, we provide an initial assessment of the efficiency of model checking to search for solutions of planning problems. To this end, we design a basic test benchmark and study the scalability of the generated SAL models in terms of plan complexity.
    Schlagwort(e): Computer Programming and Software
    Materialart: MOCHART-2008: The Fifth International Workshop on Model Checking and Artificial Inte; Jul 21, 2008 - Jul 22, 2008; Patras; Greece
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 3
    facet.materialart.
    Unbekannt
    Formally Verified Practical Algorithms for Recovery from Loss of Separation (2009)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: In this paper, we develop and formally verify practical algorithms for recovery from loss of separation. The formal verification is performed in the context of a criteria-based framework. This framework provides rigorous definitions of horizontal and vertical maneuver correctness that guarantee divergence and achieve horizontal and vertical separation. The algorithms are shown to be independently correct, that is, separation is achieved when only one aircraft maneuvers, and implicitly coordinated, that is, separation is also achieved when both aircraft maneuver. In this paper we improve the horizontal criteria over our previous work. An important benefit of the criteria approach is that different aircraft can execute different algorithms and implicit coordination will still be achieved, as long as they all meet the explicit criteria of the framework. Towards this end we have sought to make the criteria as general as possible. The framework presented in this paper has been formalized and mechanically verified in the Prototype Verification System (PVS).
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2009-215726 , L-19586 , LF99-8442
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 4
    facet.materialart.
    Unbekannt
    The ANMLite Language and Logic for Specifying Planning Problems (2007)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: We present the basic concepts of the ANMLite planning language. We discuss various aspects of specifying a plan in terms of constraints and checking the existence of a solution with the help of a model checker. The constructs of the ANMLite language have been kept as simple as possible in order to reduce complexity and simplify the verification problem. We illustrate the language with a specification of the space shuttle crew activity model that was constructed under the Spacecraft Autonomy for Vehicles and Habitats (SAVH) project. The main purpose of this study was to explore the implications of choosing a robust logic behind the specification of constraints, rather than simply proposing a new planning language.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2007-215088 , L-19405
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unbekannt
    In-Trail Procedure (ITP) Algorithm Design (2007)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: The primary objective of this document is to provide a detailed description of the In-Trail Procedure (ITP) algorithm, which is part of the Airborne Traffic Situational Awareness In-Trail Procedure (ATSA-ITP) application. To this end, the document presents a high level description of the ITP Algorithm and a prototype implementation of this algorithm in the programming language C.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/CR-2007-214863 , NIA Report No. 2007-06
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unbekannt
    A High-Level Formalization of Floating-Point Number in PVS (2006)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: We develop a formalization of floating-point numbers in PVS based on a well-known formalization in Coq. We first describe the definitions of all the needed notions, e.g., floating-point number, format, rounding modes, etc.; then, we present an application to polynomial evaluation for elementary function evaluation. The application already existed in Coq, but our formalization shows a clear improvement in the quality of the result due to the automation provided by PVS. We finally integrate our formalization into a PVS hardware-level formalization of the IEEE-854 standard previously developed at NASA.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/CR-2006-214298 , NIA-Rept-2006-01
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unbekannt
    Solving the AI Planning Plus Scheduling Problem Using Model Checking via Automatic Translation from the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL) (2007)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: This paper describes a translator from a new planning language named the Abstract Plan Preparation Language (APPL) to the Symbolic Analysis Laboratory (SAL) model checker. This translator has been developed in support of the Spacecraft Autonomy for Vehicles and Habitats (SAVH) project sponsored by the Exploration Technology Development Program, which is seeking to mature autonomy technology for the vehicles and operations centers of Project Constellation.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2007-215089 , L-19395
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unbekannt
    An Abstract Plan Preparation Language (2006)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-11
    Beschreibung: This paper presents a new planning language that is more abstract than most existing planning languages such as the Planning Domain Definition Language (PDDL) or the New Domain Description Language (NDDL). The goal of this language is to simplify the formal analysis and specification of planning problems that are intended for safety-critical applications such as power management or automated rendezvous in future manned spacecraft. The new language has been named the Abstract Plan Preparation Language (APPL). A translator from APPL to NDDL has been developed in support of the Spacecraft Autonomy for Vehicles and Habitats Project (SAVH) sponsored by the Explorations Technology Development Program, which is seeking to mature autonomy technology for application to the new Crew Exploration Vehicle (CEV) that will replace the Space Shuttle.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2006-214518 , L-19280
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unbekannt
    Rewriting Logic Semantics of a Plan Execution Language (2009)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-12
    Beschreibung: The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on the finding of two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.
    Schlagwort(e): Computer Programming and Software
    Materialart: NASA/TM-2009-215770 , L-19700 , LF99-8984
    Format: application/pdf
    Standort Signatur Erwartet Verfügbarkeit
    BibTip Andere fanden auch interessant ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unbekannt
    Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle (2009)
    In:  CASI
    Details
    Publikationsdatum: 2019-07-13
    Beschreibung: This paper presents the specification and verification in the Prototype Verification System (PVS) of a protocol intended to facilitate communication in an experimental remotely operated vehicle used by NASA researchers. The protocol is defined as a stack-layered com- position of simpler protocols. It can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process satisfies a distinct requirement. It is formally proven that the protocol components satisfy certain delivery guarantees. Compositional techniques are used to prove these guarantees also hold in the composed system. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.
    Schlagwort(e): Computer Programming and Software
    Materialart: LF99-9127 , 14th International Workshop on Formal Methods for Industrial Critical Systems; Nov 02, 2009 - Nov 03, 2009; Eindhoven; Netherlands
    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...