Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “software development framework”

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 469 records · Page 26
All sourcesNASA NTRSDOE OSTI
DOE OSTI2024

Chemical Reactivity Through Adaptive Quantum Mechanics/Many-Body Representations: Theoretical Development, Software Implementation, and Applications (Final Report)

The main objective of this research project was the development and application of a new theoretical/computational framework to model chemical transformations and electronic excitations in fluid mixtures across different phases. Our theoretical/computational framework combines our data-driven many-body (DD-MB) potentials representing molecular interactions with adaptive schemes for modeling chemical reactions in solution. The combination of these two components resulted in an adaptive quantum mechanics/many-body (adQM/MB) method that largely suppresses discontinuities between QM and MM regions, which affect existing QM/MM methods, and thus provides an accurate representation of both quantum mechanical and environmental effects through a rigorous description of mutual polarization between QM and MM regions. The implementation of our DD-MB potentials and adQM/MB method in popular software enabled computer simulations of solvation phenomena, reactive processes, and electronic excitations in fluid mixtures with chemical and spectroscopic accuracy, representing a major step toward realistic computer simulations of a wide range of molecular systems relevant to the DOE mission.

37 INORGANIC, ORGANIC, PHYSICAL, AND ANALYTICAL CH↗
NASA NTRS1994

Open architectures for formal reasoning and deductive technologies for software development

The objective of this project is to develop an open architecture for formal reasoning systems. One goal is to provide a framework with a clear semantic basis for specification and instantiation of generic components; construction of complex systems by interconnecting components; and for making incremental improvements and tailoring to specific applications. Another goal is to develop methods for specifying component interfaces and interactions to facilitate use of existing and newly built systems as 'off the shelf' components, thus helping bridge the gap between producers and consumers of reasoning systems. In this report we summarize results in several areas: our data base of reasoning systems; a theory of binding structures; a theory of components of open systems; a framework for specifying components of open reasoning system; and an analysis of the integration of rewriting and linear arithmetic modules in Boyer-Moore using the above framework.

Mccarthy, John↗
DOE OSTI2023

An Integrated Framework for Risk Assessment of Safety-related Digital Instrumentation and Control Systems in Nuclear Power Plants: Methodology Refinement and Exploration

This report documents activities performed by Idaho National Laboratory (INL) during Fiscal Year (FY) 2023 for the U.S. Department of Energy (DOE) Light Water Reactor Sustainability (LWRS) Program, Risk Informed Systems Analysis (RISA) Pathway, digital instrumentation and control (DI&C) risk assessment project. In FY 2019, the RISA Pathway initiated a project to develop a risk assessment strategy for delivering a technical basis to support effective, and secure DI&C technologies for digital upgrades/designs. A risk assessment-informed framework was proposed for this strategy, which aims to (1) provide a best-estimate, risk informed capability to quantitatively estimate the safety margin obtained from plant modernization, especially for safety-related DI&C systems, (2) support and supplement existing risk informed DI&C design guides by providing quantitative risk information and evidence, (3) offer a capability of design architecture evaluation of various DI&C systems, (4) assure the long-term safety and reliability of safety-related DI&C systems, and (5) reduce uncertainty in costs and support integration of DI&C systems in the plant. To achieve these technical goals, the LWRS-developed framework provides a means to address relevant technical issues by: (1) defining a risk informed analysis process for DI&C upgrade that integrates hazard analysis, reliability analysis, and consequence analysis, (2) applying risk informed tools to address common cause failures (CCFs) and quantify corresponding failure probabilities for DI&C technologies, particularly software CCFs, (3) evaluating the impact of digital failures at the component level, system level, and plant level, and (4) providing insights and suggestions on designs to manage the risks, thus to support the development and deployment of advanced DI&C technologies in nuclear power plants (NPPs). Adding diversity within a system or components is the primary means to eliminate and mitigate CCFs, but diversity also increases system complexity and may not address all sources of systematic failures. Optimization of diversity and redundancy applications for the safety-critical DI&C systems remains a challenge. To deal with the technical issues in addressing potential software CCFs in safety-related DI&C systems of NPPs and supporting relevant design optimization, the proposed framework provides: (a) A best-estimate, risk informed capability to address new technical digital issues quantitatively, focusing on software CCFs in safety-related DI&C systems of NPPs; (b) A common and a modularized platform for DI&C designers, software developers, cybersecurity analysts, and plant engineers to predict and prevent risk in the early design stage of DI&C systems; (c) Technical bases and risk informed insights to assist users address the risk informed alternatives for evaluation of CCFs in safety-related DI&C systems of NPPs; and (d) A risk informed tool that offers a capability of design architecture evaluation of various DI&C systems to support system design decisions in diversity and redundancy applications. The research and development efforts of this project in FY 2023 are focused on refining current methods on software CCF modeling and estimation and exploring additional innovative approaches to risk assessment of DI&C systems to enable a more comprehensive and complete assessment of various safety-related DI&C design architectures. The primary audience of this report are DI&C designers, engineers, and probabilistic risk assessment (PRA) practitioners. This includes stakeholders, such as the nuclear utilities and regulators who consider the deployment and upgrade of DI&C systems, DI&C software developers and reviewers, and cybersecurity specialists. It should be noted that all the analyses are performed for the demonstration of the methodology, not for the evaluation of an actual digital control system. Results are obtained based on limited design information and testing data.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗
NASA NTRS2003

[Development and Use of Hidrosig]

The NASA portion of this joint NSF-NASA grant consists of objective 2 and a part of objective 3. A major effort was made on objective 2, and it consisted of developing a numerical GIs environment called Hidrosig. This major research tool is being developed by the University of Colorado for conducting river-network-based scaling analyses of coupled water-energy-landform-vegetation interactions including water and energy balances, and floods and droughts, at multiple space-time scales.Objective 2: To analyze the relevant remotely sensed products from satellites, radars and ground measurements to compute the transported water mass for each complete Strahler stream using an 'assimilated water balance equation' at daily and other appropriate time scales. This objective requires analysis of concurrent data sets for Precipitation (PPT), Evapotranspiration (ET) and stream flows (Q) on river networks. To solve this major problem, our decision was to develop Hidrosig, a new Open-Source GIs software. A research group in Colombia, South America, developed the first version of Hidrosig, and Ricardo Mantilla was part of this effort as an undergraduate student before joining the graduate program at the University of Colorado in 2001. Hydrosig automatically extracts river networks from large DEMs and creates a "link-based" data structure, which is required to conduct a variety of analyses under objective 2. It is programmed in Java, which is a multi-platform programming language freely distributed by SUN under a GPL license. Some existent commercial tools like Arc-Info, RiverTools and others are not suitable for our purpose for two reasons. First, the source code is not available that is needed to build on the network data structure. Second, these tools use different programming languages that are not most versatile for our purposes. For example, RiverTools uses an IDL platform that is not very efficient for organizing diverse data sets on river networks. Hidrosig establishes a clear data organization framework that allows a simultaneous analysis of spatial fields along river network structures involving Horton- Strahler framework. Software tools for network extraction from DEMs and network-based analysis of geomorphologic and topologic variables were developed during the first year and a part of second year.

Gupta, Vijay K.↗
NASA NTRS2016

UAV Research at NASA Langley: Towards Safe, Reliable, and Autonomous Operations

Unmanned Aerial Vehicles (UAV) are fundamental components in several aspects of research at NASA Langley, such as flight dynamics, mission-driven airframe design, airspace integration demonstrations, atmospheric science projects, and more. In particular, NASA Langley Research Center (Langley) is using UAVs to develop and demonstrate innovative capabilities that meet the autonomy and robotics challenges that are anticipated in science, space exploration, and aeronautics. These capabilities will enable new NASA missions such as asteroid rendezvous and retrieval (ARRM), Mars exploration, in-situ resource utilization (ISRU), pollution measurements in historically inaccessible areas, and the integration of UAVs into our everyday lives all missions of increasing complexity, distance, pace, and/or accessibility. Building on decades of NASA experience and success in the design, fabrication, and integration of robust and reliable automated systems for space and aeronautics, Langley Autonomy Incubator seeks to bridge the gap between automation and autonomy by enabling safe autonomous operations via onboard sensing and perception systems in both data-rich and data-deprived environments. The Autonomy Incubator is focused on the challenge of mobility and manipulation in dynamic and unstructured environments by integrating technologies such as computer vision, visual odometry, real-time mapping, path planning, object detection and avoidance, object classification, adaptive control, sensor fusion, machine learning, and natural human-machine teaming. These technologies are implemented in an architectural framework developed in-house for easy integration and interoperability of cutting-edge hardware and software.

Davila, Carlos G.↗
NASA NTRS2016

Transitioning Autonomous Systems Technology Research to a Flight Software Environment

NASA has developed methods and algorithms for autonomous spacecraft operations,including automated planning and scheduling, fault diagnostics and impact determination,procedure management and display. Making the transition from technology research tooperational flight software requires overcoming significant technical, programmatic andcultural challenges. Technology research is aimed at developing methods that performspecific functions correctly, but the resulting software may not be designed for flightprocessors with limited CPU, memory and network resources, and may not be easilyintegrated into spacecraft flight software. Our objective in the Autonomous Systems andOperations Project is to make significant strides toward the transformation from technologyto operational use. Our focus was twofold: maturing research grade autonomy software intoa flight software environment using broadly accepted languages and tools; and integratingautonomy applications with each other and with representative systems and their data andcommand interfaces. For a target flight software environment, we chose Core FlightSoftware, developed by Goddard Space Flight Center as a common operating systemindependent framework. Our hardware integration environment was provided by theIntegrated Power and Avionics Systems (iPAS) Lab at Johnson Space Center, in whichvarious subsystem development has been conducted to address engineering challenges forthe vehicles and systems required for long-duration missions into the solar system. The iPASand its network of connected facilities provides realistic subsystem hardware or simulationsof spacecraft power, life support, guidance, navigation and control, and command and datahandling subsystems. Interfaces between autonomy applications and the subsystems beingassessed and controlled were developed, assessed and refined. The hardware and softwareenvironment using CFS and the iPAS facility has proven to be a highly flexible and realisticenvironment in which to rapidly integrate applications in an iterative, low cost setting. Usingthe integration environment we have developed, we will turn our focus to performance andsizing analysis to determine the computational requirements for full-scale deployment ofautonomy technology. Scalability of reasoners and the spacecraft models upon which theyoperate, and robustness across the full range of spacecraft conditions and environments willbe explored and improved. We are making significant contributions to the future programsthat will build the spacecraft that will take humans beyond the Earth-Moon system, in whichprogram Systems Engineers will be able to accurately and confidently design in accurate,robust and mature autonomous operations systems.

Flight Software↗
DOE OSTI2020

LArSoft and Future Framework Directions at Fermilab

The diversity of the scientific goals across HEP experiments necessitates unique bodies of software tailored for achieving particular physics results. The challenge, however, is to identify the software that must be unique, and the code that is unnecessarily duplicated, which results in wasted eort and inhibits code maintainability. Fermilab has a history of supporting and developing software projects that are shared among HEP experiments. Fermilab’s scientific computing division currently expends eort in maintaining and developing the LArSoft toolkit, used by liquid argon TPC experiments, as well as the event-processing framework technologies used by LArSoft, CMS, DUNE, and the majority of Fermilab-hosted experiments. As computing needs for DUNE and the HL-LHC become clearer, the computing models are being rethought. Presented here are Fermilab’s plans for addressing the evolving software landscape as it relates to LArSoft and the data-processing frameworks, specifically as it relates to the DUNE experiment.

Knoepfel, Kyle↗
DOE OSTI2016

2014 Runtime Systems Summit. Runtime Systems Report

This report summarizes runtime system challenges for exascale computing, that follow from the fundamental challenges for exascale systems that have been well studied in past reports, e.g., [6, 33, 34, 32, 24]. Some of the key exascale challenges that pertain to runtime systems include parallelism, energy efficiency, memory hierarchies, data movement, heterogeneous processors and memories, resilience, performance variability, dynamic resource allocation, performance portability, and interoperability with legacy code. In addition to summarizing these challenges, the report also outlines different approaches to addressing these significant challenges that have been pursued by research projects in the DOE-sponsored X-Stack and OS/R programs. Since there is often confusion as to what exactly the term “runtime system” refers to in the software stack, we include a section on taxonomy to clarify the terminology used by participants in these research projects. In addition, we include a section on deployment opportunities for vendors and government labs to build on the research results from these projects. Finally, this report is also intended to provide a framework for discussing future research and development investments for exascale runtime systems, and for clarifying the role of runtime systems in exascale software.

97 MATHEMATICS AND COMPUTING↗
DOE OSTI2025

Fragme∩t: An Open‐Source Framework for Multiscale Quantum Chemistry Based on Fragmentation

Fragment-based quantum chemistry offers a means to circumvent the nonlinear computational scaling of conventional electronic structure calculations, by partitioning a large calculation into smaller subsystems then considering the many-body interactions between them. Variants of this approach have been used to parameterize classical force fields and machine learning potentials, applications that benefit from interoperability between quantum chemistry codes. However, there is a dearth of software that provides interoperability yet is purpose-built to handle the combinatorial complexity of fragment-based calculations. To fill this void we introduce “Fragme∩t”, an open-source software application that provides a tool for community validation of fragment-based methods, a platform for developing new approximations, and a framework for analyzing many-body interactions. Fragme∩t includes algorithms for automatic fragment generation and structure modification, and for distance- and energy-based screening of the requisite subsystems. Checkpointing, database management, and parallelization are handled internally and results are archived in a portable database. Interfaces to various quantum chemistry engines are easy to write and exist already for Q-Chem, PySCF, xTB, Orca, CP2K, MRCC, Psi4, NWChem, GAMESS, and MOPAC. Applications reported here demonstrate parallel efficiencies around 96% on more than 1000 processors but also showcase that the code can handle large-scale protein fragmentation using only workstation hardware, all with a codebase that is designed to be usable by non-experts. Fragme∩t conforms to modern software engineering best practices and is built upon well established technologies including Python, SQLite, and Ray. The source code is available under the Apache 2.0 license.

37 INORGANIC, ORGANIC, PHYSICAL, AND ANALYTICAL CH↗
DOE OSTI2019

LArSoft and Future Framework Directions at Fermilab [Slides]

The diversity of the scientific goals across HEP experiments necessitates unique bodies of software tailored for achieving particular physics results. The challenge, however, is to identify the software that must be unique, and the code that is unnecessarily duplicated, which results in wasted effort and inhibits code maintainability. Fermilab has a history of supporting and developing software projects that are shared among HEP experiments. Fermilab's scientific computing division currently expends effort in maintaining and developing the LArSoft toolkit, used by liquid argon TPC experiments, as well as the event-processing framework technologies used by LArSoft, CMS, DUNE, and the majority of Fermilab-hosted experiments. As computing needs for DUNE and the HL-LHC become clearer, the computing models are being rethought. This talk will focus on Fermilab's plans for addressing the evolving software landscape as it relates to LArSoft and the event-processing frameworks, and how commonality among experiment software can be achieved while still supporting customizations necessary for a given experiment's physics goals.

72 PHYSICS OF ELEMENTARY PARTICLES AND FIELDS↗
DOE OSTI2018

Implementation of Software QA for SAS4A/SASSYS-1 Rev. 1

In an effort to support closure of gaps in advanced reactor licensing pathways, a multi-year task to systematically develop sodium-cooled fast reactor (SFR) codes and methods for use in a licensing framework was launched as part of the DOE-NE Advanced Reactor Technologies (ART) Program’s Regulatory Technology Development Plan (RTDP). This report documents Phase 2 of this task, which was focused on the finalization and initial implementation of a software quality assurance (SQA) program for SAS4A/SASSYS-1 and completion of high-priority SQA-related technical activities. The ultimate goal of this ongoing RTDP task is to develop an SQA framework that satisfies the fundamental requirements of relevant SQA standards and guidance while still maintaining sufficient flexibility and efficiency such that the framework can be sustained with modest resources.

22 GENERAL STUDIES OF NUCLEAR REACTORS↗
NASA NTRS2021

A Distributed Approach to High-Rate Delay Tolerant Networking Within a Virtualized Environment

The High-Rate Delay Tolerant Networking (HDTN) project has taken a distributed service-based approach to the development of a highly efficient delay tolerant networking (DTN) implementation. Through the analysis of many DTN implementations, system and mission requirements as well as the DTN protocol specifications, HDTN has worked to infuse modern computing technologies into the NASA approach to interplanetary networking. The initial use case of the HDTN software runs on a hypervisor representative of the International Space Station (ISS) DTN Gateway. In this scenario, multiple emulated payloads will send science data through HDTN to a mission operations center. HDTN will provide store and forward capability as well as network flow management. This paper discusses the infusion path of cognitive networking technologies in the NASA SCaN networks using the DTN architecture and protocols as the basis for cognitive routing and network management capabilities. HDTN has been developing the Bundle Protocol encoding and decoding mechanisms and messaging framework that can be used as the basis for integrating DTN with various learning and decision-making processes. The concepts of distributed computing, network virtualization, software defined networking and delay tolerant networking are basic building blocks which will further the development of cognitive networking. In addition to discussion of the HDTN software development and testing, this paper examines the role that each of these technologies play in the evolution of the current state of space networking into an intelligent network of networks.

Delay Tolerant Networking↗
DOE OSTI2014

Enabling a systems biology knowledgebase with gaggle and firegoose

The overall goal of this project was to extend the existing Gaggle and Firegoose systems to develop an open-source technology that runs over the web and links desktop applications with many databases and software applications. This technology would enable researchers to incorporate workflows for data analysis that can be executed from this interface to other online applications. The four specific aims were to (1) provide one-click mapping of genes, proteins, and complexes across databases and species; (2) enable multiple simultaneous workflows; (3) expand sophisticated data analysis for online resources; and enhance open-source development of the Gaggle-Firegoose infrastructure. Gaggle is an open-source Java software system that integrates existing bioinformatics programs and data sources into a user-friendly, extensible environment to allow interactive exploration, visualization, and analysis of systems biology data. Firegoose is an extension to the Mozilla Firefox web browser that enables data transfer between websites and desktop tools including Gaggle. In the last phase of this funding period, we have made substantial progress on development and application of the Gaggle integration framework. We implemented the workspace to the Network Portal. Users can capture data from Firegoose and save them to the workspace. Users can create workflows to start multiple software components programmatically and pass data between them. Results of analysis can be saved to the cloud so that they can be easily restored on any machine. We also developed the Gaggle Chrome Goose, a plugin for the Google Chrome browser in tandem with an opencpu server in the Amazon EC2 cloud. This allows users to interactively perform data analysis on a single web page using the R packages deployed on the opencpu server. The cloud-based framework facilitates collaboration between researchers from multiple organizations. We have made a number of enhancements to the cmonkey2 application to enable and improve the integration within different environments, and we have created a new tools pipeline for generating EGRIN2 models in a largely automated way.

97 MATHEMATICS AND COMPUTING↗
DOE OSTI2015

Building a Cyberinfrastructure for Environmental System Science: Modeling Frameworks, Data Management, and Scientific Workflows, Workshop Report, Potomac, Maryland, April 30-May 1, 2015

The Environmental System Science (ESS) activity within the Department of Energy’s (DOE) Office of Biological and Environmental Research (BER) seeks to advance a robust, predictive understanding of terrestrial environments, extending from bedrock to the top of the vegetative canopy and from molecular to global scales, through an iterative cycle of model-driven experimentation and observation dubbed MODEX. Considerable progress has been made toward achieving this overarching goal, but widely recognized is the fragmentation across projects and disciplines of the relevant modeling and simulation capabilities, observational and experimental data, analysis algorithms, and workflow tools. This fragmentation creates significant challenges for studying impacts and feedbacks in these complex multiscale systems. These challenges are further exacerbated by ongoing disruptive changes in high-performance computational architectures and the exponential growth in the types and volume of data that render obsolete the conventional approaches to software development and data management. Overcoming these challenges will require the development of a BER Climate and Environmental Sciences Division (CESD)–wide enabling cyberinfrastructure to support data management, cross-domain modeling, data analysis, and collaborative research. To explore the potential for working groups to initiate and guide a more integrated and community-based cyberinfrastructure, BER held the ESS Workshop on Model-Data Integration: Modeling Frameworks, Data Management, and Scientific Workflows on April 30-May 1, 2015, following the ESS Principal Investigator Meeting in Potomac, Maryland. Participants included model developers, software engineers, and data management specialists from eight national laboratories, which represented a wide range of projects and programs from CESD as well as cross-cutting projects from DOE’s Office of Advanced Scientific Computing Research (ASCR; both BER and ASCR are operated from within DOE’s Office of Science). A series of plenary talks provided background information and clarified the workshop’s three objectives: (1) develop requirements for this community-based cyberinfrastructure to ensure enhanced scientific productivity of the community as a whole; (2) identify challenges associated with developing this new cyberinfrastructure using a phased approach guided by project-driven use cases; and, given these requirements and challenges, (3) chart a path forward for ESS working groups to lead the phased development of the new cyberinfrastructure.

54 ENVIRONMENTAL SCIENCES↗
DOE OSTI2020

Annular Flow Simulation Supported by Iterative In-Memory Mesh Adaptation

Various flow regimes exist in a boiling water reactor (BWR) as the steam quality increases in the uprising coolant flow, from bubbly flow, slug/churn flow, to annular flow. The annular flow is characterized by the presence of a fast-moving gas core and the surrounding liquid film flowing on the conduit wall. Additionally, entrained droplets can be observed in the gas core with ingested bubbles in the liquid film. The dynamics occurring on the wavy interface between the liquid film and gas core plays a crucial role in affecting the heat transfer rate and pressure drop within the BWR core. However, a fundamental understanding of annular flow is still lacking, partly due to the difficulty in obtaining detailed local data in annular flow experiments. In the current study, a novel simulation framework is developed for the annular flow by coupling a computational fluid dynamics flow solver with state-of-the-art meshing software. The gas-liquid interface is tracked with the level set method. Based on the computed flow solutions, the computational mesh is dynamically adapted in memory to meet the local mesh resolution requirement. This iterative simulation-adaptation framework can ensure the fine mesh resolution across the interface, which not only helps mitigate the mass conservation degradation known to level set methods but also improves the representation of dramatic interface topological changes such as wave breaking and droplet entrainment. The present investigation will shed light onto the complex interfacial processes involved in annular flow and generate much needed simulation data for annular flow modeling.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗
DOE OSTI2014

RAVEN and Dynamic Probabilistic Risk Assessment: Software overview

RAVEN is a generic software framework to perform parametric and probabilistic analysis based on the response of complex system codes. The initial development was aimed to provide dynamic risk analysis capabilities to the Thermo-Hydraulic code RELAP-7 [], currently under development at the Idaho National Laboratory. Although the initial goal has been fully accomplished, RAVEN is now a multi-purpose probabilistic and uncertainty quantification platform, capable to agnostically communicate with any system code. This agnosticism has been employed by providing Application Programming Interfaces (APIs). These interfaces are used to allow RAVEN to interact with any code as long as all the parameters that need to be perturbed are accessible by inputs files or via python interfaces. RAVEN is capable to investigate the system response, investigating the input space using Monte Carlo, Grid, or Latin Hyper Cube sampling schemes, but its strength is focused toward system feature discovery, such as limit surfaces, separating regions of the input space leading to system failure, using dynamic supervised learning techniques. The paper presents an overview of the software capabilities and their implementation schemes followed by some application examples.

99 GENERAL AND MISCELLANEOUS↗
DOE OSTI2025

The Analysis Description Language Ecosystem: Latest developments and physics applications

We present latest developments in Analysis Description Language (ADL), a declarative domain-specific language describing the physics algorithm of a HEP data analysis decoupled from software frameworks. Analyses written in ADL can be integrated into any framework for various tasks. ADL is a multipurpose construct with uses ranging from analysis design to preservation, reinterpretation, queries, visualisation, combination, etc. The most advanced infrastructure to execute ADL on events is the CutLang runtime interpreter. Recent technical developments include an automated interface with different data types, generation of the abstract syntax tree, a visualization tool that that auto-converts analysis flows to graphs, incorporation of trained machine learning models and a Jupyter-based plotting tool. We also report physics implications including a large scale LHC analysis implementation and validation effort for beyond the standard model reinterpretation purposes and studies with ATLAS and CMS open data.

Sekmen, Sezen [Kyungpook National Univ., Daegu (Ko↗
NASA NTRS2005

Application of Lightweight Formal Methods to Software Security

Formal specification and verification of security has proven a challenging task. There is no single method that has proven feasible. Instead, an integrated approach which combines several formal techniques can increase the confidence in the verification of software security properties. Such an approach which species security properties in a library that can be reused by 2 instruments and their methodologies developed for the National Aeronautics and Space Administration (NASA) at the Jet Propulsion Laboratory (JPL) are described herein The Flexible Modeling Framework (FMF) is a model based verijkation instrument that uses Promela and the SPIN model checker. The Property Based Tester (PBT) uses TASPEC and a Text Execution Monitor (TEM). They are used to reduce vulnerabilities and unwanted exposures in software during the development and maintenance life cycles.

security↗