Results for “PVS” — Page 8

DOE OSTI2022

Real-World 20-Hz IBR Subsynchronous Oscillations: Signatures and Mechanism Analysis

This article provides analyses of subsynchronous oscillations associated with solar photovoltaics (PVs) observed in real world. All have oscillation frequencies at approximately 20 Hz in voltage and current magnitudes. On the other hand, in phase voltage and current, the oscillations show very different signatures. Through constructing simplified linear models and conducting sensitivity analysis, we are able to associate dynamic phenomena with the underlying mechanism and speculate the possible causes of the 20-Hz oscillations. The analysis results have all been validated via simulation results from electromagnetic transient (EMT) test beds constructed in MATLAB/Simscape.

inverter-based resources↗

DOE OSTI2020

Statistical Modeling of Networked Solar Resources for Assessing and Mitigating Risk of Interdependent Inverter Tripping Events in Distribution Grids

Not provided.

Engineering↗

DOE OSTI2025

Anomaly Identification of Synchronized Voltage Waveform for Situational Awareness of Low Inertia Systems

Inverter-based resources (IBRs) such as photovoltaics (PVs), wind turbines, and battery energy storage systems (BESSs) are widely deployed in low-carbon power systems. However, these resources typically do not provide the inertia needed for grid stability, resulting in a low-inertia power system. IBRs and lack of inertia have been known to cause anomalies such as waveform distortions and wideband oscillations in power systems due to the limited inertia level, leading to increased generation trips and load shedding. Here, to achieve effective anomaly identification, this paper proposes a synchro-waveform-based algorithm utilizing real-time synchronized voltage waveform measurements from waveform measurement units (WMUs). In the proposed method, different physical characteristics, as well as statistical features, are extracted from synchronized voltage waveform measurements to filter anomalies. Then, the anomaly identification approach based on the random forest is developed and deployed into the FNET/GridEye system considering trade-offs among accuracy, computational burden, and deployment cost. Moreover, four WMUs are specially designed and deployed on Kauai Island to receive instantaneous synchronized voltage waveform measurements. To verify the performance of the proposed algorithm, different experiments are carried out with collected field test data. The result demonstrates that the performance of the proposed synchro-waveform-based anomaly categorization algorithm can accurately identify anomalies 95.35% of the time, which has comparable performance among benchmarking algorithms.

Situational awareness↗

DOE OSTI2014

Multichannel response analysis on 2D projection views for detection of clustered microcalcifications in digital breast tomosynthesis

Purpose: To investigate the feasibility of a new two-dimensional (2D) multichannel response (MCR) analysis approach for the detection of clustered microcalcifications (MCs) in digital breast tomosynthesis (DBT). Methods: With IRB approval and informed consent, a data set of two-view DBTs from 42 breasts containing biopsy-proven MC clusters was collected in this study. The authors developed a 2D approach for MC detection using projection view (PV) images rather than the reconstructed three-dimensional (3D) DBT volume. Signal-to-noise ratio (SNR) enhancement processing was first applied to each PV to enhance the potential MCs. The locations of MC candidates were then identified with iterative thresholding. The individual MCs were decomposed with Hermite–Gaussian (HG) and Laguerre–Gaussian (LG) basis functions and the channelized Hotelling model was trained to produce the MCRs for each MC on the 2D images. The MCRs from the PVs were fused in 3D by a coincidence counting method that backprojects the MC candidates on the PVs and traces the coincidence of their ray paths in 3D. The 3D MCR was used to differentiate the true MCs from false positives (FPs). Finally a dynamic clustering method was used to identify the potential MC clusters in the DBT volume based on the fact that true MCs of clinical significance appear in clusters. Using two-fold cross validation, the performance of the 3D MCR for classification of true and false MCs was estimated by the area under the receiver operating characteristic (ROC) curve and the overall performance of the MCR approach for detection of clustered MCs was assessed by free response receiver operating characteristic (FROC) analysis. Results: When the HG basis function was used for MCR analysis, the detection of MC cluster achieved case-based test sensitivities of 80% and 90% at the average FP rates of 0.65 and 1.55 FPs per DBT volume, respectively. With LG basis function, the average FP rates were 0.62 and 1.57 per DBT volume at the same sensitivity levels. The difference in the two sets of basis functions for detection of MCs did not show statistical significance. Conclusions: The authors' experimental results indicate that the MCR approach is promising for the detection of MCs on PV images. The HG or LG basis functions are both effective in characterizing the signal response of MCs using the channelized Hotelling model. The coincidence counting method for fusion of the 2D MCR in 3D is an important step for FP reduction. Further study is underway to improve the MCR approach for microcalcification detection in DBT.

62 RADIOLOGY AND NUCLEAR MEDICINE↗

DOE OSTI2019

Roll-to-Roll Advanced Materials Manufacturing DOE Laboratory Collaboration - FY2018 Final Report

High-value R2R processing is used to support a wide range of products in applications which span many industrial business sectors. The overall R2R process technology can be considered as “mature” as the process methodology and has been in use for decades. This continuous processing technique traditionally involves deposition of material(s) onto moving webs or carriers or other continuous R2R, belt-fed, or conveyor-based processes that enable successive steps to build a final version which serves to support the deposited materials. Current process technologies, which typify “roll to roll”, include tape casting, silk-screen printing, reel-to-reel vacuum deposition/coating and R2R lithography. Products supported by R2R manufacturing include micro-electronics, electro-chromic window films, PVs, fuel cells for energy conversion, battery electrodes for energy storage, and barrier materials. Due to innovation in materials and process equipment, high-quality yet very low-cost multi-layer technologies can be manufactured on a very cost-competitive basis. To move energy-related products from high-cost niche applications to the commercial sector, a means must be available to enable manufacture of these products in a cost-competitive manner that is affordable by the general consumer. Fortunately, products such as fuel cells, thin- and mid-film PVs, batteries, electrochromic and piezoelectric films, water separation membranes, and other energy saving technologies readily lend themselves to manufacture using R2R approaches.Within the DOE EERE AMO, it was recognized that establishment of a program supported at the DOE National Laboratories, along with their immense design of materials and equipment modelling capabilities enabled with use of high-performance computing, could take advantage of available R2R infrastructure to manufacture new technologies. In FY 2016, a R2R Consortium was established and provided with initial “seed” funding to take an approach that was envisioned to be supportable by advanced manufacturing R2R processes. This collaborative approach was designed to foster identification and development of materials and processes related to R2R for clean-energy product development. Using computational and experimental capabilities by acknowledged subject matter experts within the supported National Laboratory system, this collaborative project would leverage the capabilities and expertise at each of four laboratories to further the development of an enabling high-volume cost-competitive platform technology. The collaboration team that is comprised of ORNL, ANL, NREL and LBNL, coordinating with EPB and other selected industry partners, was formed in April 2016 to initially address enhancing battery electrode performance and R2R manufacturing challenges. The research efforts were to predict and measure changes and results in electrode morphology and performance based on process condition changes; to evaluate mixed, active, particle size deposition and drying for novel electrode materials; to model various process condition changes and the resulting morphology and electrode performance; and to develop and validate NDE techniques for in-line measurement of battery electrode material properties. These efforts carried through FY 2017 and completed at the end of FY 2018.The approach was to look at compositions of materials with different particle sizes to make electrode samples using a R2R manufacturing process. The shape, size, and morphology of the materials, the chemistry of the formulation, the nature of slurries, their coating rate, the rate of drying all play a role in determining the final coating architecture, quality, and performance. A commercial cathode material was selected to make a series of cathodes and anodes by single pass, dual pass and slot die methods. Analysis of all the compiled results for this battery electrode development were that the best performing cathodes included: dual-pass electrode with large particles near the foil, mixed small and large particles, and small particles only. Whereas, the best performing anodes were with a mix of small and large graphite particles. An additional core project was added in FY 2017 to conduct studies of fuel cell materials that can be produced using R2R processes. The goal of this project is to explore, understand and optimize material and process parameters to support increased throughput, increased quality, and reduced cost for high volume production of gas-diffusion electrodes (GDEs) for PEMFCs. Project work in FY 2018 were to use a R2R process to fabricate electrodes without ionomer overlayer that can produce the equivalent mass activity as spray-coated electrodes with an ionomer overlayer. Oxygen-limiting current measurements were utilized to optimize oxygen mass transport. Alcohol-rich solvents were investigated, and results were that the alcohol and water ratio can be tuned to control ionomer distribution. Water-rich solvents produce a more dispersed ink which results in better high-current density performance.

36 MATERIALS SCIENCE↗

DOE OSTI2018

BPM Offset of NSLS-II Storage Ring Based on BBA Measurement

Beam based alignment (BBA) is the final calibration of the Beam position monitor (BPM) readings based on the quadrupole centers and it becomes essential process for the modern synchrotron light sources. For the convenient BBA implementation, usually BPMs are placed close to the quadrupoles and the beam is adjusted to pass the center of the quadrupoles. Therefore, measured BPM BBAs are, in fact, the BPM offsets relative to the quadrupole centers, and by observing their variations, we can estimate the relative movements of the BPMs. In NSLS-II, the BPM BBAs are measured whenever the beam-time allows and the variations are being observed. However, because changing BBAs in the BPM readings has direct and significant impact on the machine operation as well as the user experiments, they are not applied instantly. Instead, in NSLS-II, the official BBA values are managed by the snapshot archiving and retrieving system, called MASAR (MAchine Snapshot Archiving and Retrieve), so that they are well organized and can be easily set to any stored set of BBAs values. NSLS-II is implementing MASAR as a part of EPICS control system for the convenient and mistake-free machine operation. Each snapshot is a group of key-value pairs where keys are EPICS Process Variables (PVs). The snapshots are organized by configurations where each configuration has specific PV sets. And each configuration saves snapshots with titles corresponding their purposes such as normal user operations or specific beam studies. Anyone with control system account can save snapshots and they can be restored whenever needed. One of the configurations is “SR_BPM_BBAS" and the configuration includes the set of EPICS PVs for the storage ring BPM BBA values. This configuration also includes the BBAs of the in the straight sections, called ID (insertion device) BPMs playing important roles in user experiments. The ID BPM BBAs are also directly engaged in the active interlock (AI) machine protection system, which prevents the mechanical damage from the ID radiation. However, in estimating ID BPM BBAs, because there is no quadrupoles around them, interpolations from the surrounding sector BPM BBAs are used. This note focuses on the BPM offset variations based on the BBA measurement data and does not discuss about the ID BPM BBAs because they are not the direct measures of the offsets.

36 MATERIALS SCIENCE↗

DOE OSTI2020

Roll-to-Roll Advanced Materials Manufacturing DOE Laboratory Collaboration (FY2019 Final Report)

R2R processing is used to manufacture a wide range of products for various applications which span many industrial business sectors. The overall R2R methodology has been in use for decades and this continuous technique traditionally involves deposition of material(s) onto moving webs, carriers or other continuous belt-fed or conveyor-based processes that enable successive steps to build a final version which serves to support the deposited materials. Established methods that typify R2R include tape casting, silk-screen printing, reel-to-reel vacuum deposition/coating and R2R lithography. Products supported by R2R manufacturing include micro-electronics, electro-chromic window films, PVs, fuel cells for energy conversion, battery electrodes for energy storage, and barrier and membrane materials. Due to innovation in materials and process equipment, high-quality yet very low-cost multilayer technologies have the potential to be manufactured on a very cost-competitive basis. To move energy-related products from high-cost niche applications to the commercial sector, a means must be available to enable manufacture of these products in a cost-competitive manner that is affordable. Fortunately, products such as fuel cells, thin- and mid-film PVs, batteries, electrochromic and piezoelectric films, water separation membranes, and other energy saving technologies readily lend themselves to manufacture using R2R approaches. However, more early-stage research is needed to solve the challenge of linking the materials (particles, polymers, solvents, additives) used in ink and slurry formulations, though the ink processing, coating and drying processes, to the ultimate performance of the final R2R product, especially for a process that uses multiple layers of deposition to achieve the end product.

42 ENGINEERING↗

DOE OSTI2021

Roll-to-Roll Advanced Materials Manufacturing DOE Laboratory Collaboration (FY2020 Final Report)

R2R processing is used to manufacture a wide range of products for various applications which span many industrial business sectors. The overall R2R methodology has been in use for decades and this continuous technique traditionally involves deposition of material(s) onto moving webs, carriers or other continuous belt-fed or conveyor-based processes that enable successive steps to build a final version which serves to support the deposited materials. Established methods that typify R2R processing include tape casting, silk-screen printing, reel-to-reel vacuum deposition/coating, and R2R lithography. Products supported by R2R manufacturing include micro-electronics, electro-chromic window films, PVs, fuel cells for energy conversion, battery electrodes for energy storage, and barrier and membrane materials. Due to innovation in materials and process equipment, high-quality yet very low-cost multilayer technologies have the potential to be manufactured on a very cost-competitive basis. To move energy-related products from high-cost niche applications to the commercial sector, the means must be available to enable manufacture of these products in a cost-competitive manner that is affordable. Fortunately, products such as fuel cells, thin- and mid-film PVs, batteries, electrochromic and piezoelectric films, water separation membranes, and other energy saving technologies readily lend themselves to manufacture using R2R approaches. However, more early-stage research is needed to solve the challenge of linking the materials (particles, polymers, solvents, additives) used in ink and slurry formulations and the coating and drying processes to the ultimate performance of the final R2R product, especially for a process that uses multiple layers of deposition to achieve the end product. To solve the problems associated with these challenges, the R2R Collaboration is executing a research program with outcomes that will ultimately link modeling, processing, metrology and defect detection tools, thereby directly relating the properties of constituent particles and processing conditions to the performance of final devices. This collaborative approach was designed to foster identification and development of materials and processes related to R2R for clean-energy materials development. Using computational and experimental capabilities by acknowledged subject matter experts within the supported National Laboratory system, this project leverages the capabilities and expertise at each of five National Laboratories to further the development of multilayer technologies that will enable high-volume, cost-competitive platforms. A typical R2R process has three steps: (1) mixing of particles and various constituents in a slurry, (2) coating of the ink/slurry mixture on a substrate, and (3) drying/curing and processing of the coating. Final performance of devices made via R2R processes is dependent on the active materials (e.g., electrochemical particles in battery or fuel cell electrodes) and the device structure that stems from the governing component interactions within the various steps. However, a fundamental understanding of the underlying mechanisms and phenomena is still lacking, which is why industrial-scale R2R process development and manufacturing is still largely empirical in nature. The FY 2019 through FY 2021 program addresses aspects of the following two targets from the AMO Multi-Year Program Plan: (1) Target 8.1 Develop technologies to reduce the cost per manufactured throughput of continuous R2R manufacturing processes. (A) Increasing throughput of R2R processes by 5 times for batteries (to 50 square feet per minute (50 ft 2 /min)) and capacitors and 10 times for printed electronics and the manufacture of other substrates and MEs used in support of these products. (B) Developing resolution capabilities to enable registration and alignment that will detect, align, and co-deposit multiple layers of coatings and print < 1-micron (1 µm) features using continuous process scalable for commercial production. (C) Developing scalable and reliable R2R processes for solution deposition of ultra-thin (<10 nm) films for active and passive materials. (D) Develop in-line multilayer coating technology on thin films with yields greater than 95%. (2) Target 8.2 Develop in-line instrumentation tools that will evaluate the quality of single and multilayer materials in-process. (A) Developing in-line QC technologies and methodologies for real-time identification of defects and expected product properties “in-use/application” during continuous processing at all size-scales with a focus on the “micro” and “nano” scale traces, lines, and devices, i.e., <1 μm at 300 ft./min for R2R processing in air and <10 nm at 20 ft./min for vacuum (B) Developing technologies to increase the measurement frequency of surface rheology without significant cost increases with a goal of a 10-nanometer in-line profilometry at a production rate of 100,000 square millimeters per minute (100,000 mm 2 /min).

42 ENGINEERING↗

DOE OSTI2022

Roll-to-Roll Advanced Materials Manufacturing DOE Laboratory Collaboration - Early Stage R&D: Phase 2 and FY21 (Final Report)

R2R processing is used to manufacture a wide range of products for various applications which span many industrial business sectors. The overall R2R methodology has been in use for decades and this continuous technique traditionally involves deposition of material(s) onto substrates or membranes that are on moving webs, carriers or other continuous belt-fed or conveyor-based processes that enable successive steps to build a final product. Established methods that typify R2R processing include tape casting, silk-screen printing, reel-to-reel vacuum deposition/coating, and R2R lithography. Products supported by R2R manufacturing include micro-electronics, electro-chromic window films, PVs, fuel cells for energy conversion, battery electrodes and electrolytes for energy storage, and barrier and membrane materials for decarbonization and air and water filtration. Due to innovation in materials and process equipment, high-quality yet very low-cost multilayer technologies have the potential to be manufactured on a very cost-competitive basis. To move energy-related products from high-cost niche applications to the commercial sector, the means must be available to enable manufacture of these products in a cost-competitive manner. Fortunately, products such as fuel cells, thin- and mid-film PVs, batteries, electrochromic and piezoelectric films, water separation membranes, and other energy saving technologies readily lend themselves to manufacture using R2R approaches. However, more early-stage research is needed to solve the challenge of linking the materials (particles, polymers, solvents, additives) used in ink and slurry formulations and the coating and heated drying processes to the ultimate performance of the final R2R product, especially for a process that uses multiple layers of deposition to achieve the end product.

36 MATERIALS SCIENCE↗

DOE OSTI2020

The Land Sparing, Water Surface Use Efficiency, and Water Surface Transformation of Floating Photovoltaic Solar Energy Installations

Floating photovoltaic solar energy installations (FPVs) represent a new type of water surface use, potentially sparing land needed for agriculture and conservation. However, standardized metrics for the land sparing and resource use efficiencies of FPVs are absent. These metrics are critical to understanding the environmental and ecological impacts that FPVs may potentially exhibit. Here, we compared techno-hydrological and spatial attributes of four FPVs spanning different climatic regimes. Next, we defined and quantified the land sparing and water surface use efficiency (WSUE) of each FPV. Lastly, we coined and calculated the water surface transformation (WST) using generation data at the world’s first FPV (Far Niente Winery, California). The four FPVs spare 59,555 m2 of land and have a mean land sparing ratio of 2.7:1 m2 compared to ground-mounted PVs. Mean direct and total capacity-based WSUE is 94.5 ± 20.1 SD Wm−2 and 35.2 ± 27.4 SD Wm−2, respectively. Direct and total generation-based WST at Far Niente is 9.3 and 13.4 m2 MWh−1 yr−1, respectively; 2.3 times less area than ground-mounted utility-scale PVs. Our results reveal diverse techno-hydrological and spatial attributes of FPVs, the capacity of FPVs to spare land, and the utility of WSUE and WST metrics.

14 SOLAR ENERGY↗

NASA NTRS1993

A formally verified algorithm for interactive consistency under a hybrid fault model

Consistent distribution of single-source data to replicated computing channels is a fundamental problem in fault-tolerant system design. The 'Oral Messages' (OM) algorithm solves this problem of Interactive Consistency (Byzantine Agreement) assuming that all faults are worst-cass. Thambidurai and Park introduced a 'hybrid' fault model that distinguished three fault modes: asymmetric (Byzantine), symmetric, and benign; they also exhibited, along with an informal 'proof of correctness', a modified version of OM. Unfortunately, their algorithm is flawed. The discipline of mechanically checked formal verification eventually enabled us to develop a correct algorithm for Interactive Consistency under the hybrid fault model. This algorithm withstands $a$ asymmetric, $s$ symmetric, and $b$ benign faults simultaneously, using $m+1$ rounds, provided $n is greater than 2a + 2s + b + m$, and $m\geg a$. We present this algorithm, discuss its subtle points, and describe its formal specification and verification in PVS. We argue that formal verification systems such as PVS are now sufficiently effective that their application to fault-tolerance algorithms should be considered routine.

Lincoln, Patrick↗

NASA NTRS1995

Formal verification of an avionics microprocessor

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This report discusses a project undertaken to answer some of these questions, the formal verification of the AAMPS microprocessor. This project consisted of formally specifying in the PVS language a rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show that the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.

Srivas, Mandayam, K.↗

NASA NTRS1995

Formal methods demonstration project for space applications

The Space Shuttle program is cooperating in a pilot project to apply formal methods to live requirements analysis activities. As one of the larger ongoing shuttle Change Requests (CR's), the Global Positioning System (GPS) CR involves a significant upgrade to the Shuttle's navigation capability. Shuttles are to be outfitted with GPS receivers and the primary avionics software will be enhanced to accept GPS-provided positions and integrate them into navigation calculations. Prior to implementing the CR, requirements analysts at Loral Space Information Systems, the Shuttle software contractor, must scrutinize the CR to identify and resolve any requirements issues. We describe an ongoing task of the Formal Methods Demonstration Project for Space Applications whose goal is to find an effective way to use formal methods in the GPS CR requirements analysis phase. This phase is currently under way and a small team from NASA Langley, ViGYAN Inc. and Loral is now engaged in this task. Background on the GPS CR is provided and an overview of the hardware/software architecture is presented. We outline the approach being taken to formalize the requirements, only a subset of which is being attempted. The approach features the use of the PVS specification language to model 'principal functions', which are major units of Shuttle software. Conventional state machine techniques form the basis of our approach. Given this background, we present interim results based on a snapshot of work in progress. Samples of requirements specifications rendered in PVS are offered to illustration. We walk through a specification sketch for the principal function known as GPS Receiver State processing. Results to date are summarized and feedback from Loral requirements analysts is highlighted. Preliminary data is shown comparing issues detected by the formal methods team versus those detected using existing requirements analysis methods. We conclude by discussing our plan to complete the remaining activities of this task.

Divito, Ben L.↗

NASA NTRS1997

Fourth NASA Langley Formal Methods Workshop

This publication consists of papers presented at NASA Langley Research Center's fourth workshop on the application of formal methods to the design and verification of life-critical systems. Topic considered include: Proving properties of accident; modeling and validating SAFER in VDM-SL; requirement analysis of real-time control systems using PVS; a tabular language for system design; automated deductive verification of parallel systems. Also included is a fundamental hardware design in PVS.

Holloway, C. Michael↗

NASA NTRS1999

Formal Verification of the AAMP-FV Microcode

This report describes the experiences of Collins Avionics & Communications and SRI International in formally specifying and verifying the microcode in a Rockwell proprietary microprocessor, the AAMP-FV, using the PVS verification system. This project built extensively on earlier experiences using PVS to verify the microcode in the AAMP5, a complex, pipelined microprocessor designed for use in avionics displays and global positioning systems. While the AAMP5 experiment demonstrated the technical feasibility of formal verification of microcode, the steep learning curve encountered left unanswered the question of whether it could be performed at reasonable cost. The AAMP-FV project was conducted to determine whether the experience gained on the AAMP5 project could be used to make formal verification of microcode cost effective for safety-critical and high volume devices.

Miller, Steven P.↗

NASA NTRS1998

Cooperation Among Theorem Provers

This is a final report, which supports NASA's PECSEE (Persistent Cognizant Software Engineering Environment) effort and complements the Kestrel Institute project "Inference System Integration via Logic Morphism". The ultimate purpose of the project is to develop a superior logical inference mechanism by combining the diverse abilities of multiple cooperating theorem provers. In many years of research, a number of powerful theorem-proving systems have arisen with differing capabilities and strengths. Resolution theorem provers (such as Kestrel's KITP or SRI's, SNARK) deal with first-order logic with equality but not the principle of mathematical induction. The Boyer-Moore theorem prover excels at proof by induction but cannot deal with full first-order logic. Both are highly automated but cannot accept user guidance easily. The PVS system (from SRI) in only automatic within decidable theories, but it has well-designed interactive capabilities: furthermore, it includes higher-order logic, not just first-order logic. The NuPRL system from Cornell University and the STeP system from Stanford University have facilities for constructive logic and temporal logic, respectively - both are interactive. It is often suggested - for example, in the anonymous "QED Manifesto"-that we should pool the resources of all these theorem provers into a single system, so that the strengths of one can compensate for the weaknesses of others, and so that effort will not be duplicated. However, there is no straightforward way of doing this, because each system relies on its own language and logic for its success. Thus. SNARK uses ordinary first-order logic with equality, PVS uses higher-order logic. and NuPRL uses constructive logic. The purpose of this project, and the companion project at Kestrel, has been to use the category-theoretic notion of logic morphism to combine systems with different logics and languages. Kestrel's SPECWARE system has been the vehicle for the implementation.

Waldinger, Richard J.↗

NASA NTRS2004

Model Checking Failed Conjectures in Theorem Proving: A Case Study

Interactive mechanical theorem proving can provide high assurance of correct design, but it can also be a slow iterative process. Much time is spent determining why a proof of a conjecture is not forthcoming. In some cases, the conjecture is false and in others, the attempted proof is insufficient. In this case study, we use the SAL family of model checkers to generate a concrete counterexample to an unproven conjecture specified in the mechanical theorem prover, PVS. The focus of our case study is the ROBUS Interactive Consistency Protocol. We combine the use of a mechanical theorem prover and a model checker to expose a subtle flaw in the protocol that occurs under a particular scenario of faults and processor states. Uncovering the flaw allows us to mend the protocol and complete its general verification in PVS.

Pike, Lee↗

NASA NTRS2009

A Test Generation Framework for Distributed Fault-Tolerant Algorithms

Heavyweight formal methods such as theorem proving have been successfully applied to the analysis of safety critical fault-tolerant systems. Typically, the models and proofs performed during such analysis do not inform the testing process of actual implementations. We propose a framework for generating test vectors from specifications written in the Prototype Verification System (PVS). The methodology uses a translator to produce a Java prototype from a PVS specification. Symbolic (Java) PathFinder is then employed to generate a collection of test cases. A small example is employed to illustrate how the framework can be used in practice.

Goodloe, Alwyn↗