Engineering Papers⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20210023170

Using Computational Reflection in PVS

Aaron Dutle
View original source ↗Export metadata ↓

Abstract

Computational reflection is a well-known and powerful way to speed up the proof process in an interactive theorem prover. This presentation introduces the concept using PVS, and showcases 2 of the strategies using the method.

Explore related subjects

formal methodscomputational reflection

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Aaron Dutle. Using Computational Reflection in PVS. https://ntrs.nasa.gov/citations/20210023170

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

KEEP EXPLORING

Related reports

NASA NTRS2023

Automated Verification of Programmable Logic Controller Programs Against Structured Natural Language Requirements

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

formal methods↗
NASA NTRS2003

Addressing software security and mitigations in the life cycle

Traditionally, security is viewed as an organizational and Information Technology (IIJ systems function comprising of Firewalls, intrusion detection systems (IDS), system security settings and patches to the operating system (OS) and applications running on it. Until recently, little thought has been given to the importance of security as a formal approach in the software life cycle. The Jet Propulsion Laboratory has approached the problem through the development of an integrated formal Software Security Assessment Instrument (SSAI) with six foci for the software life cycle.

formal methods↗