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
Filter
  • Computer Programming and Software
Collection
Keywords
Years
  • 1
    facet.materialart.
    Unknown
    Developing User Strategies in PVS: A Tutorial (2003)
    In:  CASI
    Details
    Publication Date: 2018-06-11
    Description: This tutorial provides an overview of the PVS strategy language, and explains how to define new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses several useful techniques that can be used in developing user strategies, and provides examples that illustrate many of these techniques.
    Keywords: Computer Programming and Software
    Type: Design and Application of Strategies/Tactics in Higher Order Logics; 16-42; NASA/CP-2003-212448
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 2
    facet.materialart.
    Unknown
    Simulation and Verification of Synchronous Set Relations in Rewriting Logic (2011)
    In:  CASI
    Details
    Publication Date: 2019-07-27
    Description: This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property veri cation of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm veri cation techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the veri cation of temporal properties of a synchronous system.
    Keywords: Computer Programming and Software
    Type: NF1676L-12963 , Brazilian Symposium on Formal Methods; 26-30 Sept. 2011; Sao Paulo; Brazil
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 3
    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
  • 4
    facet.materialart.
    Unknown
    Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective (2016)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.
    Keywords: Computer Programming and Software
    Type: NF1676L-24045
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 5
    facet.materialart.
    Unknown
    Rewriting Modulo SMT (2013)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: Combining symbolic techniques such as: (i) SMT solving, (ii) rewriting modulo theories, and (iii) model checking can enable the analysis of infinite-state systems outside the scope of each such technique. This paper proposes rewriting modulo SMT as a new technique combining the powers of (i)-(iii) and ideally suited to model and analyze infinite-state open systems; that is, systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism due to the system, and external non-determinism due to the environment. They are not amenable to finite-state model checking analysis because they typically are infinite-state. By being reducible to standard rewriting using reflective techniques, rewriting modulo SMT can both naturally model and analyze open systems without requiring any changes to rewriting-based reachability analysis techniques for closed systems. This is illustrated by the analysis of a real-time system beyond the scope of timed automata methods.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2013-218033 , L-20315 , NF1676L-17235
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 6
    facet.materialart.
    Unknown
    From Verified Models to Verifiable Code (2009)
    In:  CASI
    Details
    Publication Date: 2019-07-12
    Description: 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.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2009-215943 , L-19766 , LF99-9439
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 7
    facet.materialart.
    Unknown
    Explicit Substitutions and All That (2000)
    In:  CASI
    Details
    Publication Date: 2019-08-17
    Description: Explicit substitution calculi are extensions of the lambda-calculus where the substitution mechanism is internalized into the theory. This feature makes them suitable for implementation and theoretical study of logic-based tools such as strongly typed programming languages and proof assistant systems. In this paper we explore new developments on two of the most successful styles of explicit substitution calculi: the lambda sigma- and lambda S(e)-calculi.
    Keywords: Computer Programming and Software
    Type: AD-A385383 , ICASE-2000-45 , NASA-CR-2000-210621
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 8
    facet.materialart.
    Unknown
    Real Automation in the Field (2001)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: We provide a package of strategies for automation of non-linear arithmetic in PVS. In particular, we describe a simplication procedure for the field of real numbers and a strategy for cancellation of common terms.
    Keywords: Computer Programming and Software
    Type: NASA/CR-2001-211271 , NAS 1.26:211271 , ICASE-39
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 9
    facet.materialart.
    Unknown
    On the Formal Verification of Conflict Detection Algorithms (2001)
    In:  CASI
    Details
    Publication Date: 2019-07-10
    Description: Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new systems that are significantly more autonomous than the older ones. In this paper, we present an innovative approach, based on formal verification, for establishing the correctness of conflict detection systems. Fundamental to our approach is the concept of trajectory, which is a continuous path in the x-y plane constrained by physical laws and operational requirements. From the Model of trajectories, we extract, and formally prove, high level properties that can serve as a framework to analyze conflict scenarios. We use the Airborne Information for Lateral Spacing (AILS) alerting algorithm as a case study of our approach.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2001-210864 , L-18083 , NAS 1.15:210864
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    NASA TECHNICAL REPORTS
  • 10
    facet.materialart.
    Unknown
    Theorem Proving In Higher Order Logics (2002)
    In:  CASI
    Details
    Publication Date: 2019-07-13
    Description: The TPHOLs International Conference serves as a venue for the presentation of work in theorem proving in higher-order logics and related areas in deduction, formal specification, software and hardware verification, and other applications. Fourteen papers were submitted to Track B (Work in Progress), which are included in this volume. Authors of Track B papers gave short introductory talks that were followed by an open poster session. The FCM 2002 Workshop aimed to bring together researchers working on the formalisation of continuous mathematics in theorem proving systems with those needing such libraries for their applications. Many of the major higher order theorem proving systems now have a formalisation of the real numbers and various levels of real analysis support. This work is of interest in a number of application areas, such as formal methods development for hardware and software application and computer supported mathematics. The FCM 2002 consisted of three papers, presented by their authors at the workshop venue, and one invited talk.
    Keywords: Computer Programming and Software
    Type: NASA/CP-2002-211736 , NAS 1.55:211736 , L-18211 , Track B Proceedings of the 15th International Conference on Theorem Proving In Higher Order Logics: TPHOLs 2002; Aug 20, 2002 - Aug 23, 2002; Hampton, VA; United States|Formalising Continuous Mathematics: FCM 2002; Aug 19, 2002; 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...