Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “logic”

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 1,315 records · Page 73
All sourcesNASA NTRSDOE OSTI
NASA NTRS2011

NASA Planning for Orion Multi-Purpose Crew Vehicle Ground Operations

The NASA Orion Ground Processing Team was originally formed by the Kennedy Space Center (KSC) Constellation (Cx) Project Office's Orion Division to define, refine and mature pre-launch and post-landing ground operations for the Orion human spacecraft. The multidisciplined KSC Orion team consisted of KSC civil servant, SAIC, Productivity Apex, Inc. and Boeing-CAPPS engineers, project managers and safety engineers, as well as engineers from Constellation's Orion Project and Lockheed Martin Orion Prime contractor. The team evaluated the Orion design configurations as the spacecraft concept matured between Systems Design Review (SDR), Systems Requirement Review (SRR) and Preliminary Design Review (PDR). The team functionally decomposed prelaunch and post-landing steps at three levels' of detail, or tiers, beginning with functional flow block diagrams (FFBDs). The third tier FFBDs were used to build logic networks and nominal timelines. Orion ground support equipment (GSE) was identified and mapped to each step. This information was subsequently used in developing lower level operations steps in a Ground Operations Planning Document PDR product. Subject matter experts for each spacecraft and GSE subsystem were used to define 5th - 95th percentile processing times for each FFBD step, using the Delphi Method. Discrete event simulations used this information and the logic network to provide processing timeline confidence intervals for launch rate assessments. The team also used the capabilities of the KSC Visualization Lab, the FFBDs and knowledge of the spacecraft, GSE and facilities to build visualizations of Orion pre-launch and postlanding processing at KSC. Visualizations were a powerful tool for communicating planned operations within the KSC community (i.e., Ground Systems design team), and externally to the Orion Project, Lockheed Martin spacecraft designers and other Constellation Program stakeholders during the SRR to PDR timeframe. Other operations planning tools included Kaizen/Lean events, mockups and human factors analysis. The majority of products developed by this team are applicable as KSC prepares 21st Century Ground Systems for the Orion Multi-Purpose Crew Vehicle and Space Launch System.

Letchworth, Gary↗
NASA NTRS2011

MOSFET Switching Circuit Protects Shape Memory Alloy Actuators

A small-footprint, full surface-mount-component printed circuit board employs MOSFET (metal-oxide-semiconductor field-effect transistor) power switches to switch high currents from any input power supply from 3 to 30 V. High-force shape memory alloy (SMA) actuators generally require high current (up to 9 A at 28 V) to actuate. SMA wires (the driving element of the actuators) can be quickly overheated if power is not removed at the end of stroke, which can damage the wires. The new analog driver prevents overheating of the SMA wires in an actuator by momentarily removing power when the end limit switch is closed, thereby allowing complex control schemes to be adopted without concern for overheating. Either an integral pushbutton or microprocessor-controlled gate or control line inputs switch current to the actuator until the end switch line goes from logic high to logic low state. Power is then momentarily removed (switched off by the MOSFET). The analog driver is suited to use with nearly any SMA actuator.

Gummin, Mark A.↗
NASA NTRS2007

My Rewarding Summer Research Experience at NASA

My summer research experience at the Kennedy Space Center has been a truly rewarding one. As an electrical engineering student at the University of South Florida, I was blessed with a beneficial opportunity to gain valuable knowledge in my career, and also apply it through working at NASA. One of my inspirations in becoming an engineer is to work at NASA someday, and I was very excited and honored to have this opportunity. My goal in this internship was to strengthen my preparation in becoming an engineer by learning new material, acquiring skills by practicing what I learned, and discovering the expectations of engineering work at NASA. Through this summer research, I was able to learn new computer programs and perform various tasks that gave me experience and skills as an engineer. My primary job was to conduct work on the Constellation Test article, which is a simulation model of the Crew Launch Vehicle (CLV) tanking system. This is a prototype of a launch facility and an Ares I Vehicle, which God willing will transport astronauts to the moon. Construction of the CLV is in progress and a test launch is anticipated for 2010. Moreover, the Test Article serves as a demonstration too, training test bed, and may be expanded for new simulation of launch system elements, which could be applied to real life operations. The test article is operated and run by a Programmable Logic Controller (PLC), which is a digital computer that is used to control all forms of machinery such as those in manufacturing buildings and other industries. PLCs are different than other computers because of the physical protection they have against damaging environmental conditions that would destroy other computers. Also, PLCs are equipped with lots of input and output connections that allow extensive amounts of commands to be executed, which would normally require many computers to do. Therefore, PLCs are small, rugged, and extremely powerful tools that may continue to be employed at NASA. Furthermore, in order to conduct productive work on the Test Article, I needed to learn the computer program called RS Logics 5000.

Aviles, Andres↗
NASA NTRS2012

Radiation-Hard SpaceWire/Gigabit Ethernet-Compatible Transponder

A radiation-hard transponder was developed utilizing submicron/nanotechnology from IBM. The device consumes low power and has a low fabrication cost. This device utilizes a Plug-and-Play concept, and can be integrated into intra-satellite networks, supporting SpaceWire and Gigabit Ethernet I/O. A space-qualified, 100-pin package also was developed, allowing space-qualified (class K) transponders to be delivered within a six-month time frame. The novel, optical, radiation-tolerant transponder was implemented as a standalone board, containing the transponder ASIC (application specific integrated circuit) and optical module, with an FPGA (field-programmable gate array) friendly parallel interface. It features improved radiation tolerance; high-data-rate, low-power consumption; and advanced functionality. The transponder utilizes a patented current mode logic library of radiation-hardened-by-architecture cells. The transponder was developed, fabricated, and radhard tested up to 1 MRad. It was fabricated using 90-nm CMOS (complementary metal oxide semiconductor) 9 SF process from IBM, and incorporates full BIT circuitry, allowing a loop back test. The low-speed parallel LVCMOS (lowvoltage complementary metal oxide semiconductor) bus is compatible with Actel FPGA. The output LVDS (low-voltage differential signaling) interface operates up to 1.5 Gb/s. Built-in CDR (clock-data recovery) circuitry provides robust synchronization and incorporates two alarm signals such as synch loss and signal loss. The ultra-linear peak detector scheme allows on-line control of the amplitude of the input signal. Power consumption is less than 300 mW. The developed transponder with a 1.25 Gb/s serial data rate incorporates a 10-to-1 serializer with an internal clock multiplication unit and a 10-1 deserializer with internal clock and data recovery block, which can operate with 8B10B encoded signals. Three loop-back test modes are provided to facilitate the built-in-test functionality. The design is based on a proprietary library of differential current switching logic cells implemented in the standard 90-nm CMOS 9SF technology from IBM. The proprietary low-power LVDS physical interface is fully compatible with the SpaceWire standard, and can be directly connected to the SFP MSA (small form factor pluggable Multiple Source Agreement) optical transponder. The low-speed parallel interfaces are fully compatible with the standard 1.8 V CMOS input/output devices. The utilized proprietary annular CMOS layout structures provide TID tolerance above 1.2 MRad. The complete chip consumes less than 150 mW of power from a single 1.8-V positive supply source.

Katzman, Vladimir↗
NASA NTRS2012

Security Data Warehouse Application

The Security Data Warehouse (SDW) is used to aggregate and correlate all JSC IT security data. This includes IT asset inventory such as operating systems and patch levels, users, user logins, remote access dial-in and VPN, and vulnerability tracking and reporting. The correlation of this data allows for an integrated understanding of current security issues and systems by providing this data in a format that associates it to an individual host. The cornerstone of the SDW is its unique host-mapping algorithm that has undergone extensive field tests, and provides a high degree of accuracy. The algorithm comprises two parts. The first part employs fuzzy logic to derive a best-guess host assignment using incomplete sensor data. The second part is logic to identify and correct errors in the database, based on subsequent, more complete data. Host records are automatically split or merged, as appropriate. The process had to be refined and thoroughly tested before the SDW deployment was feasible. Complexity was increased by adding the dimension of time. The SDW correlates all data with its relationship to time. This lends support to forensic investigations, audits, and overall situational awareness. Another important feature of the SDW architecture is that all of the underlying complexities of the data model and host-mapping algorithm are encapsulated in an easy-to-use and understandable Perl language Application Programming Interface (API). This allows the SDW to be quickly augmented with additional sensors using minimal coding and testing. It also supports rapid generation of ad hoc reports and integration with other information systems.

Vernon, Lynn R.↗
NASA NTRS2012

Hemispherical Field-of-View Above-Water Surface Imager for Submarines

A document discusses solutions to the problem of submarines having to rise above water to detect airplanes in the general vicinity. Two solutions are provided, in which a sensor is located just under the water surface, and at a few to tens of meter depth under the water surface. The first option is a Fish Eye Lens (FEL) digital-camera combination, situated just under the water surface that will have near-full- hemisphere (360 azimuth and 90 elevation) field of view for detecting objects on the water surface. This sensor can provide a three-dimensional picture of the airspace both in the marine and in the land environment. The FEL is coupled to a camera and can continuously look at the entire sky above it. The camera can have an Active Pixel Sensor (APS) focal plane array that allows logic circuitry to be built directly in the sensor. The logic circuitry allows data processing to occur on the sensor head without the need for any other external electronics. In the second option, a single-photon sensitive (photon counting) detector-array is used at depth, without the need for any optics in front of it, since at this location, optical signals are scattered and arrive at a wide (tens of degrees) range of angles. Beam scattering through clouds and seawater effectively negates optical imaging at depths below a few meters under cloudy or turbulent conditions. Under those conditions, maximum collection efficiency can be achieved by using a non-imaging photon-counting detector behind narrowband filters. In either case, signals from these sensors may be fused and correlated or decorrelated with other sensor data to get an accurate picture of the object(s) above the submarine. These devices can complement traditional submarine periscopes that have a limited field of view in the elevation direction. Also, these techniques circumvent the need for exposing the entire submarine or its periscopes to the outside environment.

Hemmati, Hamid↗
NASA NTRS2012

Modeling Auditory-Haptic Interface Cues from an Analog Multi-line Telephone

The Western Electric Company produced a multi-line telephone during the 1940s-1970s using a six-button interface design that provided robust tactile, haptic and auditory cues regarding the "state" of the communication system. This multi-line telephone was used as a model for a trade study comparison of two interfaces: a touchscreen interface (iPad)) versus a pressure-sensitive strain gauge button interface (Phidget USB interface controllers). The experiment and its results are detailed in the authors' AES 133rd convention paper " Multimodal Information Management: Evaluation of Auditory and Haptic Cues for NextGen Communication Dispays". This Engineering Brief describes how the interface logic, visual indications, and auditory cues of the original telephone were synthesized using MAX/MSP, including the logic for line selection, line hold, and priority line activation.

Begault, Durand R.↗
NASA NTRS2013

Implementing a Microcontroller Watchdog with a Field-Programmable Gate Array (FPGA)

Reliability is crucial to safety. Redundancy of important system components greatly enhances reliability and hence safety. Field-Programmable Gate Arrays (FPGAs) are useful for monitoring systems and handling the logic necessary to keep them running with minimal interruption when individual components fail. A complete microcontroller watchdog with logic for failure handling can be implemented in a hardware description language (HDL.). HDL-based designs are vendor-independent and can be used on many FPGAs with low overhead.

Straka, Bartholomew↗
NASA NTRS2013

Minimal Power Latch for Single-Slope ADCs

Column-parallel analog-to-digital converters (ADCs) for imagers involve simultaneous operation of many ADCs. Single-slope ADCs are well adapted to this use because of their simplicity. Each ADC contains a comparator, comparing its input signal level to an increasing reference signal (ramp). When the ramp is equal to the input, the comparator triggers a latch that captures an encoded counter value (code). Knowing the captured code, the ramp value and hence the input signal are determined. In a column-parallel ADC, each column contains only the comparator and the latches; the ramp and code generation are shared. In conventional latch or flip-flop circuits, there is an input stage that tracks the input signal, and this stage consumes switching current every time the input changes. With many columns, many bits, and high code rates, this switching current can be substantial. It will also generate noise that may corrupt the analog signals. A latch was designed that does not track the input, and consumes power only at the instant of latching the data value. The circuit consists of two S-R (set-reset) latches, gated by the comparator. One is set by high data values and the other by low data values. The latches are cross-coupled so that the first one to set blocks the other. In order that the input data not need an inversion, which would consume power, the two latches are made in complementary polarity. This requires complementary gates from the comparator, instead of complementary data values, but the comparator only triggers once per conversion, and usually has complementary outputs to begin with. An efficient CMOS (complementary metal oxide semiconductor) implementation of this circuit is shown in the figure, where C is the comparator output, D is the data (code), and Q0 and Q1 are the outputs indicating the capture of a zero or one value. The latch for Q0 has a negative-true set signal and output, and is implemented using OR-AND-INVERT logic, while the latch for Q1 uses positive- true signals and is implemented using AND-OR-INVERT logic. In this implementation, both latches are cleared when the comparator is reset. Two redundant transistors are removed from the reset side of each latch, making for a compact layout. CMOS imagers with column-parallel ADCs have demonstrated high performance for remote sensing applications. With this latch circuit, the power consumption and noise can be further reduced. This innovation can be used in CMOS imagers and very-low-power electronics

Hancock, Bruce R.↗
NASA NTRS2013

Remote Memory Access Protocol Target Node Intellectual Property

The MagnetoSpheric Multiscale (MMS) mission had a requirement to use the Remote Memory Access Protocol (RMAP) over its SpaceWire network. At the time, no known intellectual property (IP) cores were available for purchase. Additionally, MMS preferred to implement the RMAP functionality with control over the low-level details of the design. For example, not all the RMAP standard functionality was needed, and it was desired to implement only the portions of the RMAP protocol that were needed. RMAP functionality had been previously implemented in commercial off-the-shelf (COTS) products, but the IP core was not available for purchase. The RMAP Target IP core is a VHDL (VHSIC Hardware Description Language description of a digital logic design suitable for implementation in an FPGA (field-programmable gate array) or ASIC (application-specific integrated circuit) that parses SpaceWire packets that conform to the RMAP standard. The RMAP packet protocol allows a network host to access and control a target device using address mapping. This capability allows SpaceWire devices to be managed in a standardized way that simplifies the hardware design of the device, as well as the development of the software that controls the device. The RMAP Target IP core has some features that are unique and not specified in the RMAP standard. One such feature is the ability to automatically abort transactions if the back-end logic does not respond to read/write requests within a predefined time. When a request times out, the RMAP Target IP core automatically retracts the request and returns a command response with an appropriate status in the response packet s header. Another such feature is the ability to control the SpaceWire node or router using RMAP transactions in the extended address range. This allows the SpaceWire network host to manage the SpaceWire network elements using RMAP packets, which reduces the number of protocols that the network host needs to support.

Haddad, Omar↗
NASA NTRS2013

Development and Implementation of Efficiency-Improving Analysis Methods for the SAGE III on ISS Thermal Model Originating

The Stratospheric Aerosol and Gas Experiment III (SAGE III) instrument is the fifth in a series of instruments developed for monitoring aerosols and gaseous constituents in the stratosphere and troposphere. SAGE III will be delivered to the International Space Station (ISS) via the SpaceX Dragon vehicle in 2015. A detailed thermal model of the SAGE III payload has been developed in Thermal Desktop (TD). Several novel methods have been implemented to facilitate efficient payload-level thermal analysis, including the use of a design of experiments (DOE) methodology to determine the worst-case orbits for SAGE III while on ISS, use of TD assemblies to move payloads from the Dragon trunk to the Enhanced Operational Transfer Platform (EOTP) to its final home on the Expedite the Processing of Experiments to Space Station (ExPRESS) Logistics Carrier (ELC)-4, incorporation of older models in varying unit sets, ability to change units easily (including hardcoded logic blocks), case-based logic to facilitate activating heaters and active elements for varying scenarios within a single model, incorporation of several coordinate frames to easily map to structural models with differing geometries and locations, and streamlined results processing using an Excel-based text file plotter developed in-house at LaRC. This document presents an overview of the SAGE III thermal model and describes the development and implementation of these efficiency-improving analysis methods.

Liles, Kaitlin↗
NASA NTRS2013

Space Images for NASA JPL Android Version

This software addresses the demand for easily accessible NASA JPL images and videos by providing a user friendly and simple graphical user interface that can be run via the Android platform from any location where Internet connection is available. This app is complementary to the iPhone version of the application. A backend infrastructure stores, tracks, and retrieves space images from the JPL Photojournal and Institutional Communications Web server, and catalogs the information into a streamlined rating infrastructure. This system consists of four distinguishing components: image repository, database, server-side logic, and Android mobile application. The image repository contains images from various JPL flight projects. The database stores the image information as well as the user rating. The server-side logic retrieves the image information from the database and categorizes each image for display. The Android mobile application is an interfacing delivery system that retrieves the image information from the server for each Android mobile device user. Also created is a reporting and tracking system for charting and monitoring usage. Unlike other Android mobile image applications, this system uses the latest emerging technologies to produce image listings based directly on user input. This allows for countless combinations of images returned. The backend infrastructure uses industry-standard coding and database methods, enabling future software improvement and technology updates. The flexibility of the system design framework permits multiple levels of display possibilities and provides integration capabilities. Unique features of the software include image/video retrieval from a selected set of categories, image Web links that can be shared among e-mail users, sharing to Facebook/Twitter, marking as user's favorites, and image metadata searchable for instant results.

Nelson, Jon D.↗
NASA NTRS2013

Creating and Testing Simulation Software

The goal of this project is to learn about the software development process, specifically the process to test and fix components of the software. The paper will cover the techniques of testing code, and the benefits of using one style of testing over another. It will also discuss the overall software design and development lifecycle, and how code testing plays an integral role in it. Coding is notorious for always needing to be debugged due to coding errors or faulty program design. Writing tests either before or during program creation that cover all aspects of the code provide a relatively easy way to locate and fix errors, which will in turn decrease the necessity to fix a program after it is released for common use. The backdrop for this paper is the Spaceport Command and Control System (SCCS) Simulation Computer Software Configuration Item (CSCI), a project whose goal is to simulate a launch using simulated models of the ground systems and the connections between them and the control room. The simulations will be used for training and to ensure that all possible outcomes and complications are prepared for before the actual launch day. The code being tested is the Programmable Logic Controller Interface (PLCIF) code, the component responsible for transferring the information from the models to the model Programmable Logic Controllers (PLCs), basic computers that are used for very simple tasks.

Heinich, Christina M.↗
NASA NTRS2014

High Speed, Low Cost Telemetry Access from Space Development Update on Programmable Ultra Lightweight System Adaptable Radio (PULSAR)

Software Defined Radio (SDR) technology has been proven in the commercial sector since the early 1990's. Today's rapid advancement in mobile telephone reliability and power management capabilities exemplifies the effectiveness of the SDR technology for the modern communications market. In contrast, the foundations of transponder technology presently qualified for satellite applications were developed during the early space program of the 1960's. Conventional transponders are built to a specific platform and must be redesigned for every new bus while the SDR is adaptive in nature and can fit numerous applications with no hardware modifications. A SDR uses a minimum amount of analog / Radio Frequency (RF) components to up/down-convert the RF signal to/from a digital format. Once the signal is digitized, all processing is performed using hardware or software logic. Typical SDR digital processes include; filtering, modulation, up/down converting and demodulation. NASA Marshall Space Flight Center (MSFC) Programmable Ultra Lightweight System Adaptable Radio (PULSAR) leverages existing MSFC SDR designs and commercial sector enhanced capabilities to provide a path to a radiation tolerant SDR transponder. These innovations (1) reduce the cost of NASA Low Earth Orbit (LEO) and Deep Space standard transponders, (2) decrease power requirements, and (3) commensurately reduce volume. A second pay-off is the increased SDR flexibility by allowing the same hardware to implement multiple transponder types simply by altering hardware logic - no change of hardware is required - all of which will ultimately be accomplished in orbit. Development of SDR technology for space applications will provide a highly capable, low cost transponder to programs of all sizes. The MSFC PULSAR Project results in a Technology Readiness Level (TRL) 7 low-cost telemetry system available to Smallsat and CubeSat missions, as well as other platforms. This paper documents the continued development and verification/validation of the MSFC SDR, called PULSAR, which contributes to advancing the state-of-the-art in transponder design - directly applicable to the SmallSat and CubeSat communities. This paper focuses on lessons learned on the first sub-orbital flight (high altitude balloon) and the follow-on steps taken to validate PULSAR. A sounding rocket launch, currently planned for 03/2015, will further expose PULSAR to the high dynamics of sub-orbital flights. Future opportunities for orbiting satellite incorporation reside in the small satellite missions (FASTSat, CubeSat. etc.).

Simms, William Herbert, III↗
NASA NTRS2013

The Collection 6 'dark-target' MODIS Aerosol Products

Aerosol retrieval algorithms are applied to Moderate resolution Imaging Spectroradiometer (MODIS) sensors on both Terra and Aqua, creating two streams of decade-plus aerosol information. Products of aerosol optical depth (AOD) and aerosol size are used for many applications, but the primary concern is that these global products are comprehensive and consistent enough for use in climate studies. One of our major customers is the international modeling comparison study known as AEROCOM, which relies on the MODIS data as a benchmark. In order to keep up with the needs of AEROCOM and other MODIS data users, while utilizing new science and tools, we have improved the algorithms and products. The code, and the associated products, will be known as Collection 6 (C6). While not a major overhaul from the previous Collection 5 (C5) version, there are enough changes that there are significant impacts to the products and their interpretation. In its entirety, the C6 algorithm is comprised of three sub-algorithms for retrieving aerosol properties over different surfaces: These include the dark-target DT algorithms to retrieve over (1) ocean and (2) vegetated-dark-soiled land, plus the (3) Deep Blue (DB) algorithm, originally developed to retrieve over desert-arid land. Focusing on the two DT algorithms, we have updated assumptions for central wavelengths, Rayleigh optical depths and gas (H2O, O3, CO2, etc.) absorption corrections, while relaxing the solar zenith angle limit (up to 84) to increase pole-ward coverage. For DT-land, we have updated the cloud mask to allow heavy smoke retrievals, fine-tuned the assignments for aerosol type as function of season location, corrected bugs in the Quality Assurance (QA) logic, and added diagnostic parameters such as topographic altitude. For DT-ocean, improvements include a revised cloud mask for thin-cirrus detection, inclusion of wind speed dependence in the retrieval, updates to logic of QA Confidence flag (QAC) assignment, and additions of important diagnostic information. At the same time as we have introduced algorithm changes, we have also accounted for upstream changes including: new instrument calibration, revised land-sea masking, and changed cloud masking. Upstream changes also impact the coverage and global statistics of the retrieved AOD. Although our responsibility is to the DT code and products, we have also added a product that merges DT and DB product over semi-arid land surfaces to provide a more gap-free dataset, primarily for visualization purposes. Preliminary validation shows that compared to surface-based sunphotometer data, the C6, Level 2 (along swath) DT-products compare at least as well as those from C5. C6 will include new diagnostic information about clouds in the aerosol field, including an aerosol cloud mask at 500 m resolution, and calculations of the distance to the nearest cloud from clear pixels. Finally, we have revised the strategy for aggregating and averaging the Level 2 (swath) data to become Level 3 (gridded) data. All together, the changes to the DT algorithms will result in reduced global AOD (by 0.02) over ocean and increased AOD (by 0.02) over land, along with changes in spatial coverage. Changes in calibration will have more impact to Terras time series, especially over land. This will result in a significant reduction in artificial differences in the Terra and Aqua datasets, and will stabilize the MODIS data as a target for AEROCOM studie

Aerosol retrieval algorithms↗
NASA NTRS2014

Microscale Digital Vacuum Electronic Gates

Systems and methods in accordance with embodiments of the invention implement microscale digital vacuum electronic gates. In one embodiment, a microscale digital vacuum electronic gate includes: a microscale field emitter that can emit electrons and that is a microscale cathode; and a microscale anode; where the microscale field emitter and the microscale anode are disposed within at least a partial vacuum; where the microscale field emitter and the microscale anode are separated by a gap; and where the potential difference between the microscale field emitter and the microscale anode is controllable such that the flow of electrons between the microscale field emitter and the microscale anode is thereby controllable; where when the microscale anode receives a flow of electrons, a first logic state is defined; and where when the microscale anode does not receive a flow of electrons, a second logic state is defined.

Manohara, Harish↗
NASA NTRS2009

Proof-Carrying Code with Correct Compilers

In the late 1990s, proof-carrying code was able to produce machine-checkable safety proofs for machine-language programs even though (1) it was impractical to prove correctness properties of source programs and (2) it was impractical to prove correctness of compilers. But now it is practical to prove some correctness properties of source programs, and it is practical to prove correctness of optimizing compilers. We can produce more expressive proof-carrying code, that can guarantee correctness properties for machine code and not just safety. We will construct program logics for source languages, prove them sound w.r.t. the operational semantics of the input language for a proved-correct compiler, and then use these logics as a basis for proving the soundness of static analyses.

Appel, Andrew W.↗
NASA NTRS2012

Semantically-Rigorous Systems Engineering Modeling Using Sysml and OWL

The Systems Modeling Language (SysML) has found wide acceptance as a standard graphical notation for the domain of systems engineering. SysML subsets and extends the Unified Modeling Language (UML) to define conventions for expressing structural, behavioral, and analytical elements, and relationships among them. SysML-enabled modeling tools are available from multiple providers, and have been used for diverse projects in military aerospace, scientific exploration, and civil engineering. The Web Ontology Language (OWL) has found wide acceptance as a standard notation for knowledge representation. OWL-enabled modeling tools are available from multiple providers, as well as auxiliary assets such as reasoners and application programming interface libraries, etc. OWL has been applied to diverse projects in a wide array of fields. While the emphasis in SysML is on notation, SysML inherits (from UML) a semantic foundation that provides for limited reasoning and analysis. UML's partial formalization (FUML), however, does not cover the full semantics of SysML, which is a substantial impediment to developing high confidence in the soundness of any conclusions drawn therefrom. OWL, by contrast, was developed from the beginning on formal logical principles, and consequently provides strong support for verification of consistency and satisfiability, extraction of entailments, conjunctive query answering, etc. This emphasis on formal logic is counterbalanced by the absence of any graphical notation conventions in the OWL standards. Consequently, OWL has had only limited adoption in systems engineering. The complementary strengths and weaknesses of SysML and OWL motivate an interest in combining them in such a way that we can benefit from the attractive graphical notation of SysML and the formal reasoning of OWL. This paper describes an approach to achieving that combination.

Web Ontology Language (OWL)↗