- Technical Report
- GALOIS-02-11-A
- Feb 2021
US Patent Number 8,195,599
The present disclosure includes methods, devices, and systems for inferring system-level properties. One or more embodiments include generating a constraint model based on a system model having a number of components at different levels of abstraction and on a number of verified component properties. The constraint model can include a number of mission constraints modeling one or more mission requirements, a number of system constraints modeling one or more system-level properties, mid a number of component constraints modeling one or more component properties. One or more embodiments can include analyzing the constraint model with a constraint solver to determine whether one or more particular system-level properties can be inferred from the constraint model.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
We are concerned with the problem of optimizing network resource allocations to mission tasks. The model includes unreliable network assets, multiple mission tasks and phases,and the possibility of over-provisioning one or more tasks as a means of increasing the likelihood of task success. In this paper, we describe an implemented approach to optimizing network resources so as to optimize the expected utility of the mission. This differs significantly from previous work on cloud and network management, where the objective was to optimize some operational measure of the network itself, rather than the effect of network failures on a specific task. The work described here is preliminary: we describe the problem and the approach, define an architecture, and present the current state of the implementation.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
The present disclosure includes systems and methods for route planning. As an example, a computer implemented method for route planning can include generating a first portion of a planned route between a first location and a second location by assembling a set of previously traversed route segments each corresponding to one or more of a number of previously traversed routes, aggregating the set of previously traversed route segments with a number of route segments determined by a model-based route planning subsystem and corresponding to a second portion of the planned route, and causing the planned route to be provided to a display of a computing device.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
In this paper, we describe a set of software tools called the PRIDE ONTOlogy Editor (PRONTOE) and a methodology that allows system operators and domain experts to build and maintain ontologies of their systems with no explicit understanding of the underlying ontology representation. We present two case studies: one using NASA flight controllers, and another using the DARPA Robotic Challenge.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
A fundamental requirement for success with technology that supports space operations, such as automated procedures and interactive plan generation, is that the technology must operate on valid models or ontologies of the application domain. Making these models is difficult because the data involved are voluminous, dynamic and come from a variety of sources and formats, so manual entry and maintenance is prohibitive. Using an ontological framework such as OWL can greatly alleviate this effort, but domain experts reason in domain terms, not the formal logic of ontologies. This paper describes an editing system that allows NASA domain experts to construct and maintain ontological information, and yet produce a standard form that can be manipulated by procedure authoring and execution, automated planning and other AI applications.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
In this paper, we describe a specific approach to iterative planning in the domain of off-road route planning, in which the objective is to find a cost-minimal path from one point to another. In iterative planning we are concerned with finding a way to solve a succession of planning problems, improving the system’s behavior over time. For example, this improvement might come about through improved heuristics, leading to more effective search of the space of possible plans, or through corrections or additions to the domain model used in planning. In this work, we take the latter approach, modifying the domain model based on differences between plans generated using the existing model and “good” plans.
Read More
- Technical Report
- GALOIS-02-11-A
- Feb 2021
Real-time performance is a critical aspect of avionics computing. The Basic Avionics Lightweight Source Archetype (BALSA) exemplar provides a collection of Units of Conformance (UoCs) backed by a Future Airborne Capability Environment™ (FACE) Unit of Portability (UoP) Supplied Model (USM) running in a Linux desktop environment. This gives an easy-to-run example for users of the FACE Technical Standard and effectively illustrates the conformance aspects of the FACE Technical Standard, but is not intended to run with hard real-time constraints. To address this limitation, we developed Basswood, a BALSA-based exemplar using components aligned to the FACE Technical Standard running in a real-time environment. Basswood runs on Real-Time Executive for Multiprocessor Systems (RTEMS), an open source Real-time Operating System (RTOS). Further, Basswood facilitates a practical demonstration of model-based systems engineering using the Architecture Analysis and Design Language (AADL). Basswood helps demonstrate how combined use of the FACE Technical Standard and AADL allows application of virtual integration analysis methods to FACE UoCs. This paper describes the lessons we learned adapting BALSA to a real-time environment and introduces readers to virtual integration analysis with the FACE Technical Standard and AADL.
Read More
- Technical Report
- GALOIS-21-01
- Jan 2021
As secure multi-party computation (MPC) moves into the mainstream, users will expect it to support familiar data types such as IEEE-754 standard floating-point representations. Today, however, MPC typically does not support that standard. Instead, MPC implementations generally support alternative real number representations that are more amenable to MPC computation. In this paper, we compare performance of IEEE-754 floating point in MPC with those alternative representations, and we show that IEEE-754 may not perform well enough in MPC to be a wise choice.
Read More
- Technical Report
- GALOIS-12-28-A
- Dec 2020
Challenging problems associated with system software complexity growth are threatening industry’s ability to build next-generation safety-critical embedded systems, including helicopter avionics systems. Contributors to these problems include the growth of software, system integration, and interaction complexity exacerbated by ambiguous, missing, incomplete, and inconsistent requirements. Problems continue to hamper systems in the areas of resource utilization, timing, safety, and security. A new approach called the Architecture-Centric Virtual Integration Process (ACVIP), which is based on Society of Automotive Engineers (SAE) Standard AS5506A Architecture Analysis and Design Language (AADL), is being developed and investigated by the U.S. Army to address these challenges. ACVIP is a quantitative, architecture-centric, model-based approach enabling virtual integration analysis in the early phases and throughout the lifecycle to detect and remove defects that currently are not found until software and systems integration and acceptance testing. In an effort to investigate such an approach, the government, in conjunction with researchers from the Carnegie Mellon University (CMU) Software Engineering Institute (SEI) and Adventium Labs®, is conducting ACVIP requirements, safety, and timing analyses in parallel with the Joint Common Architecture (JCA) Demonstration (Demo).
Read More
- Technical Report
- GALOIS-12-28-A
- Dec 2020
In traditional design methodologies, the system designer typically develops the application in a sequential paradigm almost to completion before addressing issues of parallelism and mapping to a heterogeneous architecture. As the architectural complexity of these applications increase, however, this process becomes too costly since implementation must be started anew after the design. The quality of the design also often suffers as a result. This is especially true for embedded applications, where the complexity lies within the system software and hardware architecture. We present a new methodology and toolset aimed at improving the system development process for high-performance embedded applications. The toolset provides a unified design representation from early design specification to integration—allowing for parallelism and synchronization specification in domain specific styles, and automating many process steps such as partitioning/mapping, simulation, glue-code generation, and performance analysis.
Read More