IKOS: Sound Static Program Analysis

Guillaume Brat

NASA NTRS · 20220007431

IKOS: Sound Static Program Analysis

Abstract

This is a tutorial on how to use the IKOS tool for static analysis of C/C++ code for flight critical system. The tutorial explains what static code analysis is, what kind of errors IKOS can find, and how to use the tool on single or multiple file projects. Simple examples are given to illustrate the use of the tool. This tutorial also describes the use of IKOS on real mission code, in this case, the flight software for the BioSentinel mission and the Troupe project in the Robust Software Engineering group.

Explore related subjects

Aviation Software assurance Static code analysis

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Guillaume Brat. IKOS: Sound Static Program Analysis. https://ntrs.nasa.gov/citations/20220007431

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2023

SafeAeroBERT: Towards a Safety-Informed Aerospace-Specific Language Model

As aviation systems continue to operate with high traffic, large amounts of documents containing safety-relevant data continue to be generated via reporting systems such as the ASRS. Advanced natural language processing techniques, specifically pre-trained language models, have shown great success in domain-specific applications; however, the text in aviation safety reports is inundated with jargon and thus not fully utilized by general pre-trained models. In this research, we work towards developing a safety-informed aerospace-specific language model by pre-training a Bidirectional Encoder Representations from Transformer (BERT) model on reports from the Aviation Safety Reporting System and the National Transportation Safety Board. The resulting model, called SafeAeroBERT, is fine-tuned for the specific task of document classification, and can be further tuned for named-entity recognition, relation detection, information retrieval, and summarization. Results from the classification task are compared between SafeAeroBERT, the base BERT, and SciBERT models and show SafeAeroBERT outperforms the general BERT and SciBERT on classifying reports about human factors, aircraft, and procedure. SafeAeroBERT can be used on custom tasks, not limited to document classification, and is intended to aid an intelligent knowledge manager for safety report repositories.

Aviation↗

NASA NTRS2019

Application of AI in the NAS - the Rationale for AI-Enhanced Airspace Management

This paper extends on the initial findings of "Application of Artificial Intelligence in the National Airspace System: A Primer" (Stroup & Niewoehner: Herndon, VA; ICNS-2019), and looks at why the current technologies, enterprise architecture, and future program plans may not be enough to address persistent operational challenges. This paper further explores why emergent operational concepts, business models, and demand profiles may necessitate AI-enhanced Communications, Navigation and Communications (CNS) infrastructure to disrupt current operational impediments. European airspace, as well as the NAS, has similar challenges. Key challenges explored in this study include: quantifiable improvements to NAS capacity, efficiency, and resiliency; traffic flow management of diverse users; UTM-ATM airspace integration; equitable access to airspace; and airborne-ground interoperability of AI applications. Finally, we examine why trustworthiness and resiliency will be key mileposts on the regulatory pathway to AI certification.

Aviation↗

NASA NTRS2014

A Framework for Dimensioning VDL-2 Air-Ground Networks

This paper describes a framework developed at MITRE for dimensioning a Very High Frequency (VHF) Digital Link Mode 2 (VDL-2) Air-to-Ground network. This framework was developed to support the FAA's Data Communications (Data Comm) program by providing estimates of expected capacity required for the air-ground network services that will support Controller-Pilot-Data-Link Communications (CPDLC), as well as the spectrum needed to operate the system at required levels of performance. The Data Comm program is part of the FAA's NextGen initiative to implement advanced communication capabilities in the National Airspace System (NAS). The first component of the framework is the radio-frequency (RF) coverage design for the network ground stations. Then we proceed to describe the approach used to assess the aircraft geographical distribution and the data traffic demand expected in the network. The next step is the resource allocation utilizing optimization algorithms developed in MITRE's Spectrum ProspectorTM tool to propose frequency assignment solutions, and a NASA-developed VDL-2 tool to perform simulations and determine whether a proposed plan meets the desired performance requirements. The framework presented is capable of providing quantitative estimates of multiple variables related to the air-ground network, in order to satisfy established coverage, capacity and latency performance requirements. Outputs include: coverage provided at different altitudes; data capacity required in the network, aggregated or on a per ground station basis; spectrum (pool of frequencies) needed for the system to meet a target performance; optimized frequency plan for a given scenario; expected performance given spectrum available; and, estimates of throughput distributions for a given scenario. We conclude with a discussion aimed at providing insight into the tradeoffs and challenges identified with respect to radio resource management for VDL-2 air-ground networks.

Aviation↗