Engineering Papers⌕ Search

Engineering topics

Swee Balachandran

Publications and source records attributed to Swee Balachandran.

18 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2022

Towards an Implementation of Differential Dynamic Logic in PVS

This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, which employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification process. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

Differential Dynamic Logic↗
NASA NTRSDate not supplied

Autonomous Spacecraft Inspection with Free-Flying Drones

This paper describes a proof-of-concept mission demonstrating a multi-agent system performing visual inspection of damage sustained by a spacecraft. Free-flying satellites, simulated by unmanned aerial vehicles (UAVs), autonomously fly around a mock space module maximizing the search space for damage detection. The free-flyers are responsible for independently coordinating their flights to avoid collision with the space module and each other, while executing mission tasks. Damage analysis on the surface of the mock space module is performed in real-time using video from each free-flyer. Three-dimensional modeling is deployed offline to supplement and improve damage detection. This approach demonstrates the feasibility of deploying real space systems for damage detection, where 2D analysis can quickly determine region of interest and 3D visualization can produce a human-navigable virtual environment with depth perspective for further investigation.

unmanned aerial vehicle (UAV)↗
NASA NTRSDate not supplied

From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems(ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods↗
NASA NTRSDate not supplied

Monitoring ICAROUS: From Requirements to Autonomous Flight

The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.

Formal Methods↗
NASA NTRSDate not supplied

SIRIUS: Simulation Infrastructure for Research on Interoperating Unmanned Systems

This paper presents the Simulation Infrastructure for Research on Interoperating Unmanned Systems (SIRIUS), a research framework for simulation and analysis of future conceptual Urban Air Mobility (UAM) operations. SIRIUS is being developed under the auspices of the NASA Air Traffic Management eXploration project, UAM subproject (ATM-X UAM). SIRIUS provides an intuitive, highly configurable graphical user interface to design complex traffic scenarios and airspace configurations representative of conceptual UAM operations. Aircraft simulated with SIRIUS can be equipped with flight-tested capabilities for detect and avoid (DAA), geofencing, distributed merging and spacing, path conformance, and path planning while executing time-constrained, 4D trajectories generated by a UAM ground operations system. Central to the design of the SIRIUS simulation framework is the capability to evaluate the integration and interoperability of ground-based separation services (e.g., strategic separation) with extended DAA functionality (e.g., path monitoring, separation provision, merging and spacing, etc.) The simulation environment also supports modelling of wind, navigation, and sensor uncertainties, as well as communication delays. SIRIUS enables distributed simulation of large-scale scenarios. An interactive graphical analysis capability helps isolate, visualize, and compare relevant vehicle state data and widely used measures of performance metrics across multiple scenarios.

Andrew Peters↗
NASA NTRSDate not supplied

Formal Specification and Parametric Verification of the ICAROUS Distributed Merging Protocol for Autonomous Aircraft Systems

ICAROUS is a software architecture that provides highly assured core software modules for building safety-centric autonomous unmanned aircraft applications. One of its core components is the ICAROUS distributed merging (IDM) protocol, which allows for decentralized merging of autonomous aircrafts through a designated intersection. This report presents initial results on formal specification and parametric verification of the IDM protocol. We present the development of a formal, discrete-time specification of the ICAROUS distributed merging protocol in TLA+. The developed TLA+ specification includes an abstracted model of the physical aircraft dynamics, the consensus machinery for leader election and coordination, and the computation of merging schedules. In addition, we present details on a command line tool we developed verimerge, that utilizes the TLC model checker for doing bounded, parametric verification and allows for plotting of these results in 2D parameter spaces. The tool also provides functionality for visualization of concrete protocol behaviors, to aid debugging and understanding. We present preliminary, bounded time verification results for a finite number of aircraft. Limitations of the current techniques and possible future extensions of this work are also discussed.

ICAROUS↗
NASA NTRSDate not supplied

Embedding Differential Dynamic Logic in PVS

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL’s proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.

PVS↗
NASA NTRSDate not supplied

Embedding Differential Dynamic Logic in PVS

Runtime assurance is a control framework where a complex controller operates under the observation of a monitor. If the monitor detects the controller exhibiting undesirable behavior, control is passed off to a trusted controller until a desirable state is regained. The runtime assurance architecture provides a layer of assurance to the system being controlled, but special care must be taken that the resulting overall system, consisting of the monitors and controllers, is behaving as intended. This talk aims to formally model and reason about runtime assurance-equipped systems as hybrid programs- which are models that consist of both discrete and continuous components. Using the verification tool Plaidypvs, safety properties of some examples involving RTA architectures is shown.

Formal Verification↗