search menu icon-carat-right cmu-wordmark
2023 Research Review

Formal Arguments for Large-Scale Assurance (FALSA)

Re-assurance of evolving large-scale systems can bottleneck deployment of new capability the U.S. Department of Defense (DoD) needs for new missions and environments. This presents a challenge for the speed and confidence required to deploy capability. Large DoD platform programs must spend extensive time and resources to repeat analysis and testing to re-assure their systems before each software release. Even future systems that better leverage model-based software engineering (MBSE) approaches plan to extensively repeat analysis and testing for each software release. Overcoming this re-assurance problem is key to enabling mission resiliency.

This project is the first in a sequence of projects that aims to reduce the time and effort to re-assure DoD systems by making advances in the design and automated evaluation of formal assurance arguments. The ability to use formal assurance frameworks to guide software development in a way that will dramatically reduce the time from innovation to deployment requires advances in several areas, including designing and representing assurance arguments; using runtime data in conjunction with assurance arguments to make runtime adaptation decisions (for example, to adapt to new missions, changes in available resources); and using runtime experience to refine assurance arguments.

This is the first in a sequence of projects that aims to reduce the time and effort to re-assure DoD systems.

Dr. Gabriel Moreno
Principal Researcher
Dr. Gabriel Moreno

This project aimed to speed up the assurance of evolving large-scale systems through two approaches:

  • reuse and sound integration of diverse assurance analyses
  • rapid detection of nonconformance between the system behavior and its assurance argument

For the first approach, we used modal logic informed by rules that determine when it is correct to combine assurance analyses and results of different types in an assurance argument. These rules also define how to evaluate this combination. Since many important military systems are cyber-physical systems, the dynamics of how a system moves through the physical world is obviously important. For that reason, in the second approach to this project, we focused on physical correctness. In particular, we used scientific machine learning and deep operator networks to be able to predict trajectories of a drone in real time based on the non-linear dynamics of the system. This allows us to check physical correctness in real time.

The work in this project serves as a foundation for future work. In FY24, we will focus on the composition of assurance arguments of subsystems independently developed, with the detection and resolution of conflicts that might arise.

Speeding Up the Assurance of Evolving Large-Scale Systems Speeding Up the Assurance of Evolving Large-Scale Systems

In Context: This FY2023 Project

  • is a collaborative effort with researchers from Carnegie Mellon University‚Äôs Department of Electrical and Computer Engineering
  • aligns with the CMU SEI technical objectives to be trustworthy in construction and implementation, and to be timely so that the DoD is able to field new software-enabled systems and their upgrades faster than our adversaries
  • aligns with the OUSD(R&E) priority of leveraging advanced computing and software technologies