Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “formal”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 109 records · Page 6
All sourcesNASA NTRSDOE OSTI
NASA NTRS2006

Ten Commandments of Formal Methods...Ten Years Later

More than a decade ago, in "Ten Commandments of Formal Methods," we offered practical guidelines for projects that sought to use formal methods. Over the years, the article, which was based on our knowledge of successful industrial projects, has been widely cited and has generated much positive feedback. However, despite this apparent enthusiasm, formal methods use has not greatly increased, and some of the same attitudes about the infeasibility of adopting them persist. Formal methodists believe that introducing greater rigor will improve the software development process and yield software with better structure, greater maintainability, and fewer errors.

Bowen, Jonathan P.↗
NASA NTRS1994

Initiating Formal Requirements Specifications with Object-Oriented Models

This paper reports results of an investigation into the suitability of object-oriented models as an initial step in developing formal specifications. The requirements for two critical system-level software modules were used as target applications. It was found that creating object-oriented diagrams prior to formally specifying the requirements enhanced the accuracy of the initial formal specifications and reduced the effort required to produce them. However, the formal specifications incorporated some information not found in the object-oriented diagrams, such as higher-level strategy or goals of the software.

requirements specifications↗
NASA NTRS2009

Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code

We present an approach to systematically derive safety cases for automatically generated code from information collected during a formal, Hoare-style safety certification of the code. This safety case makes explicit the formal and informal reasoning principles, and reveals the top-level assumptions and external dependencies that must be taken into account; however, the evidence still comes from the formal safety proofs. It uses a generic goal-based argument that is instantiated with respect to the certified safety property (i.e., safety claims) and the program. This will be combined with a complementary safety case that argues the safety of the framework itself, in particular the correctness of the Hoare rules with respect to the safety property and the trustworthiness of the certification system and its individual components. Keywords: Automated code generation, Hoare logic, formal code certification, safety case, Goal Structuring Notation.

Basir, Nurlida↗
NASA NTRS2012

An Ontology for State Analysis: Formalizing the Mapping to SysML

State Analysis is a methodology developed over the last decade for architecting, designing and documenting complex control systems. Although it was originally conceived for designing robotic spacecraft, recent applications include the design of control systems for large ground-based telescopes. The European Southern Observatory (ESO) began a project to design the European Extremely Large Telescope (E-ELT), which will require coordinated control of over a thousand articulated mirror segments. The designers are using State Analysis as a methodology and the Systems Modeling Language (SysML) as a modeling and documentation language in this task. To effectively apply the State Analysis methodology in this context it became necessary to provide ontological definitions of the concepts and relations in State Analysis and greater flexibility through a mapping of State Analysis into a practical extension of SysML. The ontology provides the formal basis for verifying compliance with State Analysis semantics including architectural constraints. The SysML extension provides the practical basis for applying the State Analysis methodology with SysML tools. This paper will discuss the method used to develop these formalisms (the ontology), the formalisms themselves, the mapping to SysML and approach to using these formalisms to specify a control system and enforce architectural constraints in a SysML model.

Wagner, David A.↗
NASA NTRS2015

Line Mixing in Parallel and Perpendicular Bands of CO2: A Further Test of the Refined Robert-Bonamy Formalism

Starting from the refined Robert-Bonamy formalism [Q. Ma, C. Boulet, and R. H. Tipping, J. Chem. Phys. 139, 034305 (2013)], we propose here an extension of line mixing studies to infrared absorptions of linear polyatomic molecules having stretching and bending modes. The present formalism does not neglect the internal degrees of freedom of the perturbing molecules, contrary to the energy corrected sudden (ECS) modeling, and enables one to calculate the whole relaxation matrix starting from the potential energy surface. Meanwhile, similar to the ECS modeling, the present formalism properly accounts for roles played by all the internal angular momenta in the coupling process, including the vibrational angular momentum. The formalism has been applied to the important case of CO2 broadened by N2. Applications to two kinds of vibrational bands (sigma yields sigma and sigma yields pi) have shown that the present results are in good agreement with both experimental data and results derived from the ECS model.

Semiclassical theories↗
NASA NTRS2015

Formal Foundations for Hierarchical Safety Cases

Safety cases are increasingly being required in many safety-critical domains to assure, using structured argumentation and evidence, that a system is acceptably safe. However, comprehensive system-wide safety arguments present appreciable challenges to develop, understand, evaluate, and manage, partly due to the volume of information that they aggregate, such as the results of hazard analysis, requirements analysis, testing, formal verification, and other engineering activities. Previously, we have proposed hierarchical safety cases, hicases, to aid the comprehension of safety case argument structures. In this paper, we build on a formal notion of safety case to formalise the use of hierarchy as a structuring technique, and show that hicases satisfy several desirable properties. Our aim is to provide a formal, theoretical foundation for safety cases. In particular, we believe that tools for high assurance systems should be granted similar assurance to the systems to which they are applied. To this end, we formally specify and prove the correctness of key operations for constructing and managing hicases, which gives the specification for implementing hicases in AdvoCATE, our toolset for safety case automation. We motivate and explain the theory with the help of a simple running example, extracted from a real safety case and developed using AdvoCATE.

Hierarchy↗
NASA NTRS2015

Formal Methods in Air Traffic Management: The Case of Unmanned Aircraft Systems

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.

Munoz, Cesar A.↗
NASA NTRS2019

Formalizing and Analyzing Requirements with FRET

Formal verification and simulation are powerful tools to validate requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. To this end, we have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written structured natural language.

Mavridou, Anastasia↗
NASA NTRSDate not supplied

Simplifying Requirements Formalization for Resource-Constrained Mission-Critical Software

Developing critical software requires adherence to rigorous software development practices, such as formal requirement specification and verification. Despite their importance, such practices are often considered as complex and challenging tasks that require a strong formal methods background. In this paper, we present our work on simplifying the formal requirements specification experience for resource-constrained mission critical software through the use of structured natural language. To this end, we connect NASA’s FRET, a formal requirement elicitation and authoring tool with the Shelley model checking framework for MicroPython code. We report our experience on using these tools to specify requirements and analyze code from the NASA Ames PHALANX exploration concept.

PHALANX exploration concept↗
NASA NTRS1994

Applying Formal Methods and Object-Oriented Analysis to Existing Space Shuttle Software

This paper describes the application of formal methods and object-oriented modeling to reverse engineering, in which formal specifications are developed for existing, or legacy, code. In this project, several layers of formal specifications were constructed for a portion of the NASA Space Shuttle Digital Auto Pilot (DAP), a software module that is used to control the position of the spacecraft through appropriate jet firings.

software engineering↗
NASA NTRS2013

Evidence Arguments for Using Formal Methods in Software Certification

We describe a generic approach for automatically integrating the output generated from a formal method/tool into a software safety assurance case, as an evidence argument, by (a) encoding the underlying reasoning as a safety case pattern, and (b) instantiating it using the data produced from the method/tool. We believe this approach not only improves the trustworthiness of the evidence generated from a formal method/tool, by explicitly presenting the reasoning and mechanisms underlying its genesis, but also provides a way to gauge the suitability of the evidence in the context of the wider assurance case. We illustrate our work by application to a real example-an unmanned aircraft system- where we invoke a formal code analysis tool from its autopilot software safety case, automatically transform the verification output into an evidence argument, and then integrate it into the former.

Argumentation↗
NASA NTRS2014

State Event Models for the Formal Analysis of Human-Machine Interactions

The work described in this paper was motivated by our experience with applying a framework for formal analysis of human-machine interactions (HMI) to a realistic model of an autopilot. The framework is built around a formally defined conformance relation called "fullcontrol" between an actual system and the mental model according to which the system is operated. Systems are well-designed if they can be described by relatively simple, full-control, mental models for their human operators. For this reason, our framework supports automated generation of minimal full-control mental models for HMI systems, where both the system and the mental models are described as labelled transition systems (LTS). The autopilot that we analysed has been developed in the NASA Ames HMI prototyping tool ADEPT. In this paper, we describe how we extended the models that our HMI analysis framework handles to allow adequate representation of ADEPT models. We then provide a property-preserving reduction from these extended models to LTSs, to enable application of our LTS-based formal analysis algorithms. Finally, we briefly discuss the analyses we were able to perform on the autopilot model with our extended framework.

State-event Models↗
NASA NTRSDate not supplied

Towards Formalization of Advanced Linear Algebra with Applications to Dynamical Systems using PVS

Linear Algebra is essential for numerous aerospace problems of interest. Formal reasoning about hybrid systems that contain variables modeled by differential equations rely on concepts from Linear Algebra such as eigenvalues, matrix decompositions, and matrix valued functions. For example, the long-term dynamics of a system of differential equations depend on the stability/instability of its equilibrium points, which often reduces to an eigenvalue problem. This talk will embark on a quest to formalize theorems and results about eigenvalues and eigenvectors using PVS. We shall start our journey with 2 x 2 complex matrices, where we will apply our PVS code to a simple example of a dynamical system. Since it can be difficult or impossible to give simple expressions of eigenvalues for larger matrices (i.e. 5 x 5 or higher), we then move towards specifying the power method for verified computation of eigenvalue approximations in PVS. This effort requires development of multivariate complex arithmetic. At the end of the day, having such additions to the PVS NASA libraries will help move towards the use of formal methods to verify concepts of control theory and system level verification.

Linear Algebra↗
NASA NTRSDate not supplied

Formal Analysis of the Compact Position Reporting Algorithm

This presentation documents the formal analysis of the compact position reporting (CPR) algorithm. CPR is a fundamental part of Automatic Dependent Surveillance - Broadcast (ADS-B), which is a global protocol for aircraft communication. The formal analysis found and corrected issues with the algorithm, proposed simplifications, and created a formally verified reference implementation, all of which are incorporated in the governing standards document.

Formal Methods↗
NASA NTRS2022

Characterizing Student-Driven Research Investigations Contributed to the GLOBE Program Citizen Science Initiative in a Formal Education Context

The Global Learning and Observations to Benefit the Environment (GLOBE) Program offers citizen science opportunities to participants of all ages, with a focus on youth in formal classroom contexts. This study uses student investigation research reports and posters submitted to the 2018 International Virtual Science Symposium (IVSS) and Student Research Symposium (SRS) as testbeds for characterizing student-driven Earth system citizen science investigations. Secondarily, this study aimed to capture GLOBE’s alignment to existing citizen science outcomes frameworks in the literature, which have primarily focused on adults and non-formal settings. Based on a literature review, the evaluation team identified 89 potential characteristics in 27 categories to typify investigations from both formal education and citizen science perspectives. We coded the artifacts from 207 student projects, conducted quantitative analysis of frequencies, and performed a semantic network analysis. By using this networking approach, we conceptually mapped several clusters of co-occurring characteristics, defining a descriptive framework for GLOBE projects. We identified three tiers of citizen science projects, increasing in the sophistication of participants’ demonstrated science practices. The framework includes additional components that reflect student citizen scientists’ thoughtfulness and connection to context as well as their projects’ reflection of their motivation and self efficacy. Through these findings, we have identified areas where student citizen scientists would benefit from further support, and suggest here further research to incorporate the experiences of students into the broader understanding of citizen science outcomes.

network analysis↗
NASA NTRSDate not supplied

Formalization of the Bellman-Ford Algorithm for Airspace Applications

This paper describes the formal verification of one of the most well-known algorithms for finding the shortest path between all vertices in a directed graph, namely the Bellman-Ford algorithm. This formal verification, performed in the Prototype Verification System (PVS), is motivated by two applications in the aerospace domain which use the algorithm for path planning. The first is a pre-flight calculation that uses an adapted version of Bellman-Ford to find a route intended to maximize GNSS availability throughout the flight. The second is a more traditional application intended to find the shortest path between an autonomous aircraft's current position and a goal waypoint, while avoiding regions of space specified by geofences. A novel aspect of this formal verification effort is the inclusion of two distinct models of computation for the algorithm, one being a traditional serial computation, and the other being an explicitly parallel computation. The ability to use parallel computation in the Bellman-Ford algorithm is in fact why it was chosen over other traditionally more performant algorithms, especially for the GNSS application, where the size of the graph makes a purely serial computation infeasible.

formal verification↗
DOE OSTI2024

Three-particle formalism for multiple channels: the ηππ + $ K\overline{K}\pi $ system in isosymmetric QCD

We generalize previous three-particle finite-volume formalisms to allow for multiple three-particle channels. For definiteness, we focus on the two-channel ηππ and $ K\overline{K}\pi $ system in isosymmetric QCD, considering the positive G parity sector of the latter channel, and neglecting the coupling to modes with four or more particles. The formalism we obtain is thus appropriate to study the b 1 (1235) and η(1295) resonances. The derivation is made in the generic relativistic field theory approach using the time-ordered perturbation theory method. We study how the resulting quantization condition reduces to that for a single three-particle channel when one drops below the upper ($ K\overline{K}\pi $) threshold. We also present parametrizations of the three-particle K matrices that enter into the formalism.

72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗
DOE OSTI2022

Formal verification and validation of run-to-completion style state charts using Event-B

State chart notations with ‘run to completion’ semantics are popular with engineers for designing controllers that react to environment events with a sequence of state transitions but lack formal refinement and rigorous verification methods. State chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. Abstraction and formal verification provide greater assurance that critical (e.g. safety or security) properties are not violated by the control system. In this paper, we introduce a notion of refinement into a ‘run to completion’ state chart modelling notation and leverage Event-B’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how models can be validated at different refinement levels using our scenario checker animation tools. We show how critical invariant properties can be verified by proof despite the reactive nature of the system and how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic, model checking approach. To verify liveness, we outline a proof that the run to completion is deadlock-free and converges to complete the run.

97 MATHEMATICS AND COMPUTING↗