Engineering Papers⌕ Search

Engineering topics

J. Tanner Slagel

Publications and source records attributed to J. Tanner Slagel.

7 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

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↗
NASA NTRSDate not supplied

A Temporal Differential Dynamic Logic Formal Embedding

Differential dynamic logic is a formal framework to specify and reason about hybrid programs (HPs). The core of dL is a proof calculus that contains a collection of axioms and rules for the rigorous verification of properties of HPs. Recently, dL has been embedded within the theorem prover Prototype Verification System (PVS) resulting in the tool Plaidypvs2. The integration of dL into PVS expands its expressive power; user defined functions, such as trigonometric and other transcendental functions, can be used inside the dL framework, and meta-reasoning about HPs can be performed, including reasoning about entire classes of HPs, specified using dependent types in PVS. The differential temporal dynamic logic (dTL2) extends dL with temporal logic operators to reason about all the states reachable during the execution of an HP. This paper presents a work in progress focusing on embedding dTL2 in PVS as an extension of Plaidypvs. Plaidypvs is expanded with the formalization of a trace semantics for HPs, the definition of the LTL temporal operators eventually and globally, and the implementation of the proof calculus for dTL2. This new embedding has the same capabilties as Plaidypvs, which allows user defined functions and meta-reasoning of properties of HPs. To the best of the authors’ knowledge this is the first implementation of dTL2.

differential dynamic logic↗
NASA NTRSDate not supplied

A Formal Verification Framework for Runtime Assurance

The simplex architecture is an instance of Runtime Assurance (RTA) where a trusted component takes control of a safety-critical system when an untrusted component violates a safety property. This paper presents a formalization of the simplex RTA framework in the language of hybrid programs. A feature of this formal verification framework is that, for a given system, a specific instantiation can be created and its safety properties are guaranteed by construction. Instantiations may be kept at varying levels of generality, allowing for black box components, such as ML/AI-based controllers, to be modeled. The framework is written in the Prototype Verification System (PVS) using Plaidypvs, an embedding of differential dynamic logic in PVS. As a proof of concept, the framework is illustrated on an automatic vehicle braking system.

Runtime assurance↗