Program generation and transformation systems manipulate large, pa- rameterized object language fragments. Support for user-definable concrete syntax makes this easier but is typically restricted to certain object and meta languages. We show how Prolog can be retrofitted with concrete syntax and describe how a seamless interaction of concrete syntax fragments with an existing legacy meta-programming system based on abstract syntax is achieved. We apply the approach to gradually migrate the...
Topics: NASA Technical Reports Server (NTRS), SYNTAX, COMPUTER PROGRAMS, INFORMATION ANALYSIS, MACHINE...
New and sharp estimates are derived for the growth in the complex plane of polynomials known to have a curved majorant on a given ellipse. These so-called Bernstein type inequalities are closely connected with certain constrained Chebyshev approximation problems on ellipses. Also presented are some new results for approximation problems of this type.
Topics: NASA Technical Reports Server (NTRS), CHEBYSHEV APPROXIMATION, ELLIPSES, INEQUALITIES, POLYNOMIALS,...
AutoBayes is a fully automatic, schema-based program synthesis system for statistical data analysis applications. Its core component is a schema library. i.e., a collection of generic code templates with associated applicability constraints which are instantiated in a problem-specific way during synthesis. Currently, AutoBayes is implemented in Prolog; the schemas thus use abstract syntax (i.e., Prolog terms) to formulate the templates. However, the conceptual distance between this abstract...
Topics: NASA Technical Reports Server (NTRS), COMPUTER PROGRAMS, STATISTICAL ANALYSIS, DATA PROCESSING,...
The Hoare approach to program verification relies on the construction and discharge of verification conditions (VCs) but offers no support to trace, analyze, and understand the VCs themselves. We describe a systematic extension of the Hoare rules by labels so that the calculus itself can be used to build up explanations of the VCs. The labels are maintained through the different processing steps and rendered as natural language explanations. The explanations can easily be customized and can...
Topics: NASA Technical Reports Server (NTRS), PROGRAM VERIFICATION (COMPUTERS), PROVING, NATURAL LANGUAGE...
The problem is that of finding among all polynomials of degree at most n and normalized to be 1 at c the one with minimal uniform norm on Epsilon. Here, Epsilon is a given ellipse with both foci on the real axis and c is a given real point not contained in Epsilon. Problems of this type arise in certain iterative matrix computations and, in this context, it is generally believed and widely referenced that suitably normalized Chebyshev polynomials are optimal for such constrained approximation...
Topics: NASA Technical Reports Server (NTRS), CHEBYSHEV APPROXIMATION, ITERATION, MATRICES (MATHEMATICS),...
Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea...
Topics: NASA Technical Reports Server (NTRS), PROGRAM VERIFICATION (COMPUTERS), COMPUTER PROGRAMS,...
Formal proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because the formalism in which they are constructed and encoded is usually machine-oriented, and they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to...
Topics: NASA Technical Reports Server (NTRS), FORMALISM, SOFTWARE ENGINEERING, AUTOMATION, THEOREM PROVING,...
Constrained Chebyshev approximation problems of the type with minimum (p is an element of Pi(sub n):p(c)=1) and maximum (z is an element of E) with /p(z)/ are considered. Here Pi(sub n) denotes the set of all complex polynomials of degree at most n, E is any ellipse in the complex plane, and c is an element of C/E. Such approximation problems arise in the context of optimizing semi-iterative methods for the solution of large, sparse systems of linear equations Ax=b with complex non-Hermitian...
Topics: NASA Technical Reports Server (NTRS), CHEBYSHEV APPROXIMATION, ITERATIVE SOLUTION, LINEAR...
Incremental certification and re-certification of code as it is developed and modified is a prerequisite for applying modem, evolutionary development processes, which are especially relevant for NASA. For example, the Columbia Accident Investigation Board (CAIB) report 121 concluded there is "the need for improved and uniform statistical sampling, audit, and certification processes". Also, re-certification time has been a limiting factor in making changes to Space Shuttle code close...
Topics: NASA Technical Reports Server (NTRS), CERTIFICATION, COMPUTER PROGRAMS, MANAGEMENT SYSTEMS, MODEMS,...
Model-based development and automated code generation are increasingly used for production code in safety-critical applications, but since code generators are typically not qualified, the generated code must still be fully tested, reviewed, and certified. This is particularly arduous for mathematical and control engineering software which requires reviewers to trace subtle details of textbook formulas and algorithms to the code, and to match requirements (e.g., physical units or coordinate...
Topics: NASA Technical Reports Server (NTRS), COMPUTER PROGRAMMING, NATURAL LANGUAGE (COMPUTERS), SOFTWARE...
Model-based design and automated code generation are being used increasingly at NASA. The trend is to move beyond simulation and prototyping to actual flight code, particularly in the guidance, navigation, and control domain. However, there are substantial obstacles to more widespread adoption of code generators in such safety-critical domains. Since code generators are typically not qualified, there is no guarantee that their output is correct, and consequently the generated code still needs...
Topics: NASA Technical Reports Server (NTRS), NATURAL LANGUAGE (COMPUTERS), SOFTWARE ENGINEERING, SOFTWARE...
Code certification is a lightweight approach to demonstrate software quality on a formal level. Its basic idea is to require producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates which can be checked independently. Since code certification uses the same underlying technology as program verification, it also requires many detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding theses...
Topics: NASA Technical Reports Server (NTRS), COMPUTER PROGRAMS, PROGRAM VERIFICATION (COMPUTERS),...
A viewgraph describing formal approaches taken to assure the safety of space software is presented. The topics include: 1) Certifiable Program Generation; 2) Certification Framework; 3) Annotation Generation; 4) Experiments; and 5) Future Work.
Topics: NASA Technical Reports Server (NTRS), SAFETY, SOFTWARE ENGINEERING, FORMALISM, AIRBORNE/SPACEBORNE...
Model-based design and automated code generation are increasingly used at NASA to produce actual flight code, particularly in the Guidance, Navigation, and Control domain. However, since code generators are typically not qualified, there is no guarantee that their output is correct, and consequently auto-generated code still needs to be fully tested and certified. We have thus developed AUTOCERT, a generator-independent plug-in that supports the certification of auto-generated code. AUTOCERT...
Topics: NASA Technical Reports Server (NTRS), SOFTWARE ENGINEERING, CERTIFICATION, MISSION PLANNING,...
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, and usability. For full automation, however, the obligations must be aggressively preprocessed and simplified, and we demonstrate...
Topics: NASA Technical Reports Server (NTRS), PROVING, PROGRAM VERIFICATION (COMPUTERS), SYSTEMS...
This paper presents a new methodology for automatic knowledge driven data mining based on the theory of Mercer Kernels, which are highly nonlinear symmetric positive definite mappings from the original image space to a very high, possibly dimensional feature space. we describe a new method called Mixture Density Mercer Kernels to learn kernel function directly from data, rather than using pre-defined kernels. These data adaptive kernels can encode prior knowledge in the kernel using a Bayesian...
Topics: NASA Technical Reports Server (NTRS), ALGEBRA, ALGORITHMS, BAYES THEOREM, TEMPLATES, SKY SURVEYS...
In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the...
Topics: NASA Technical Reports Server (NTRS), NATURAL LANGUAGE (COMPUTERS), SAFETY, POLICIES, INFORMATION...
We present a logical framework in which abstract interpretations can be naturally specified and then verified. Our approach is based on membership equational logic which extends equational logics by membership axioms, asserting that a term has a certain sort. We represent an abstract interpretation as a membership equational logic specification, usually as an overloaded order-sorted signature with membership axioms. It turns out that, for any term, its least sort over this specification...
Topics: NASA Technical Reports Server (NTRS), MATHEMATICAL LOGIC, INTERPRETATION, OPERATORS (MATHEMATICS),...
Program verification using Hoare-style techniques requires many logical annotations. We have previously developed a generic annotation inference algorithm that weaves in all annotations required to certify safety properties for automatically generated code. It uses patterns to capture generator- and property-specific code idioms and property-specific meta-program fragments to construct the annotations. The algorithm is customized by specifying the code patterns and integrating them with the...
Topics: NASA Technical Reports Server (NTRS), PROGRAM VERIFICATION (COMPUTERS), ALGORITHMS, FUNCTIONAL...
AUTOBAYES is a fully automatic program synthesis system for the statistical data analysis domain. Its input is a concise description of a data analysis problem in the form of a statistical model; its output is optimized and fully documented C/C++ code which can be linked dynamically into the Matlab and Octave environments. AUTOBAYES synthesizes code by a schema-guided deductive process. Schemas (i.e., code templates with associated semantic constraints) are applied to the original problem and...
Topics: NASA Technical Reports Server (NTRS), COMPUTER PROGRAMS, STATISTICAL ANALYSIS, SYMBOLIC...
We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). For full automation, however, the obligations must be aggressively preprocessed and simplified We describe the unique requirements this places on the ATP and demonstrate how the individual simplification stages, which are implemented by...
Topics: NASA Technical Reports Server (NTRS), AUTOMATIC CONTROL, THEOREM PROVING, AEROSPACE ENGINEERING,...
We describe a certification assistant to support formal safety proofs for programs. It is based on a graphical user interface that hides the low-level details of first-order automated theorem provers while supporting limited interactivity: it allows users to customize and control the proof process on a high level, manages the auxiliary artifacts produced during this process, and provides traceability between the proof obligations and the relevant parts of the program. The certification...
Topics: NASA Technical Reports Server (NTRS), CERTIFICATION, AUTOMATIC CONTROL, THEOREM PROVING, GRAPHICAL...
Mathematical models of blood flow are inevitably embedded in models of human thermoregulation because they take the role of the most significant heat distributor in models of the human thermal system 14, 6. Models of human thermoregulation have a wide range of applications, e.g. for the prediction of the impact of accidents, diseases and clinical treatments (see 14 and the references therein). The application of our interest is the prediction of the influence of cooling on the heat distribution...
Topics: DTIC Archive, Breuss, Michael, Meister, Andreas, Fischer, Bernd, HAMBURG UNIV (GEMANY) DEPT OF...
Proofs provide detailed justification for the validity of claims and are widely used in formal software development methods. However, they are often complex and difficult to understand, because they use machine-oriented formalisms; they may also be based on assumptions that are not justified. This causes concerns about the trustworthiness of using formal proofs as arguments in safety-critical applications. Here, we present an approach to develop safety cases that correspond to formal proofs...
Topics: NASA Technical Reports Server (NTRS), DECISION SUPPORT SYSTEMS, LOGIC PROGRAMMING, SOFTWARE...
The conjugate gradient algorithm for solving Hermitian positive definite linear systems is usually combined with preconditioning in order to speed up convergence. In recent years, there has been a revival of polynomial preconditioning, motivated by the attractive features of the method on modern architectures. Standard techniques for choosing the preconditioning polynomial are based only on bounds for the extreme eigenvalues. Here a different approach is proposed, which aims at adapting the...
Topics: NASA Technical Reports Server (NTRS), ALGORITHMS, CHEBYSHEV APPROXIMATION, CONJUGATE GRADIENT...
The design of iterative schemes for sparse matrix computations often leads to constrained polynomial approximation problems on sets in the complex plane. For the case of ellipses, we introduce a new class of complex polynomials which are in general very good approximations to the best polynomials and even optimal in most cases.
Topics: NASA Technical Reports Server (NTRS), CHEBYSHEV APPROXIMATION, COMPLEX VARIABLES, ELLIPSES,...
This paper presents a new methodology for automatic knowledge driven data mining based on the theory of Mercer Kernels, which are highly nonlinear symmetric positive definite mappings from the original image space to a very high, possibly infinite dimensional feature space. We describe a new method called Mixture Density Mercer Kernels to learn kernel function directly from data, rather than using predefined kernels. These data adaptive kernels can en- code prior knowledge in the kernel using a...
Topics: NASA Technical Reports Server (NTRS), NONLINEARITY, MATHEMATICAL MODELS, KNOWLEDGE BASED SYSTEMS,...
In this paper, we describe the experiences of the Automated Software Engineering Group at the NASA Ames Research Center in the development and application of three different transformation systems. The systems span the entire technology range, from deductive synthesis, to logic-based transformation, to almost compiler-like source-to-source transformation. These systems also span a range of NASA applications, including solving solar system geometry problems, generating data analysis software,...
Topics: NASA Technical Reports Server (NTRS), SOFTWARE ENGINEERING, COMPUTER PROGRAMMING, COMPILERS,...
Program synthesis is the process of automatically deriving executable code from (non-executable) high-level specifications. It is more flexible and powerful than conventional code generation techniques that simply translate algorithmic specifications into lower-level code or only create code skeletons from structural specifications (such as UML class diagrams). Key to building a successful synthesis system is specializing to an appropriate application domain. The AUTOBAYES and AUTOFILTER...
Topics: NASA Technical Reports Server (NTRS), COMPUTER SYSTEMS PROGRAMS, ARTIFICIAL INTELLIGENCE, AUTOMATIC...
Program synthesis is the systematic, automatic construction of efficient executable code from high-level declarative specifications. AutoBayes is a fully automatic program synthesis system for the statistical data analysis domain; in particular, it solves parameter estimation problems. It has seen many successful applications at NASA and is currently being used, for example, to analyze simulation results for Orion. The input to AutoBayes is a concise description of a data analysis problem...
Topics: NASA Technical Reports Server (NTRS), USER MANUALS (COMPUTER PROGRAMS), C++ (PROGRAMMING LANGUAGE),...
The purpose of this document is to propose a product-oriented software certification process to facilitate use of software synthesis and formal methods. Why is such a process needed? Currently, software is tested until deemed bug-free rather than proving that certain software properties exist. This approach has worked well in most cases, but unfortunately, deaths still occur due to software failure. Using formal methods (techniques from logic and discrete mathematics like set theory, automata...
Topics: NASA Technical Reports Server (NTRS), SOFTWARE ENGINEERING, ARCHITECTURE (COMPUTERS), PROGRAM...
