Benedetto L. Di Vito

NOTE: Ben is retired from NASA as of 20 January 2018.

Synopsis

Ben is a senior research engineer in the Safety-Critical Avionics Systems Branch at the NASA Langley Research Center. He became a NASA civil servant in November 1998. Before that, Ben was a senior research engineer at VíGYAN, Inc, where he worked as an on-site contractor at NASA Langley. He has been associated with the formal methods team since December 1989.

Research in applied formal methods and dependable computing is the focus of Ben's work. Advancing the underlying methods and tools is also a principal focus as is application areas such as aviation safety, autonomous systems, fault-tolerant computing and flight-critical avionics. He has investigated methods for automating certain classes of proofs, such as those involving real-valued arithmetic and properties of state machine models. Ben led an effort to create a database capability called Hypatheon to enhance the effectiveness of interactive proof. He has contributed to investigations on assurance techniques for numerically intensive software applications.

Under NASA's Aeronautics Research Mission Directorate, Ben is supporting the Airspace Operations and Safety Program (AOSP). In recent years he also contributed to the Aviation Safety Program and the Airspace Program. In his current assignment for AOSP, he is serving as a V&V lead on the Safe Autonomous System Operations (SASO) project. Previously he had worked as a team lead on the System-wide Safety and Assurance Technologies (SSAT) project of the Aviation Safety Program.

From 2006 to 2010, Ben supported NASA's Exploration Systems Mission Directorate. This included roles on the Systems Engineering and Integration team for the Constellation Program as well as the Automation for Operations (A4O) project, which was a research effort under the Exploration Technology Development Program.

In earlier years, Ben completed some pilot studies on the use of formal methods in space applications, and helped author the NASA formal methods guidebooks. He was also a major contributor to the Reliable Computing Platform project. In a more service-oriented role, Ben participated on NASA's Software Engineering Research Infusion team in 2004 and 2005. He has also been a long-standing member of the steering committee for NFM, the NASA Formal Methods Symposium.

Ben has interests and research experience within the general area of dependable computing, especially as it pertains to embedded systems. Related areas of interest include formal methods, software engineering, computational logic, fault tolerance, information security and trusted systems.

Background

• Education and Experience
• Publications and External Activities

Past Activities (1998 - 2004)

Ben spent some time studying the partitioning problem for integrated modular avionics (IMA). These efforts included past participation in RTCA standards committee SC-182, which created a Minimal Operating Performance Standard (MOPS) for Avionics Computer Resources (ACRs).

In 1998 Ben introduced a formal model of space (memory) partitioning, whose purpose is to state requirements for the safe integration of multiple avionics functions on a single computer platform, thereby offering assurance that such integration cannot lead to harmful interference. PVS notation was used to capture an abstract model of computation in ACRs and an expression of desirable system properties, which were subjected to proof using the PVS theorem prover.

Having previously introduced a stylized technique for modeling state machines in PVS and using it to formalize key portions of the Shuttle's GPS Change Request, Ben adapted it to formalize the embedded controller for SAFER, a backpack propulsion unit worn by NASA astronauts on certain EVAs. Taking this effort one step further, Ben developed automated prover strategies customized for high level problem domains.

The development of new prover strategies to automate aspects of theorem proving for continuous mathematics was another key activity. In 2002 Ben developed a set of algebraic manipulation strategies called Manip, with important new features being added in 2005. Manip was incorporated into PVS in version 5.0 (released April 2011).

From 2003 to 2005, Ben initiated and led a small project to establish a mathematical database service called Hypatheon. This service was to use a relational DMBS and supporting tool infrastructure to collect and disseminate PVS theories.

In 2003, 2005 and 2007, Ben led a team of researchers from NASA Langley and the National Institute of Aerospace (NIA) in teaching short courses on the PVS specification and verification system. These courses were offered to engineers from the aerospace industry as well as faculty members and their students.

From March 2004 through September 2005, Ben participated on the NASA-wide Software Engineering Research Infusion team. The goal of this team was to foster improvements in NASA's software practices by identifying emerging software technologies and awarding small pilot projects so practitioners can evaluate new tools in realistic project settings.

Past Activities (2005 - 2010)

From January 2005 through September 2006, Ben was the adviser and colleague of Dr. Songtao Xia, a post-doctoral researcher who received an appointment under the Research Associateship Programs of the National Academies. Dr. Xia has been developing techniques to apply model checkers, decision procedures, and constraint solvers to create new software assurance tools. This effort aims to derive analytical techniques and tools for examining software naturally rich in numerical calculation.

From 2006 to 2010, Ben supported NASA's Exploration Systems Mission Directorate. In the first role, he was a member of the Systems Engineering and Integration team on the Constellation Program from June 2006 through September 2007, where he was helping to refine the program-level requirements.

In the second role, from 2006 through 2010 he was the co-lead for Verification and Validation on the Automation for Operations (A4O) project, which was a research effort under the Exploration Technology Development Program. Efforts under A4O emphasized the use of formal methods to validate electronic procedures and automated planning models.

Prior to the current structure of the Aviation Safety program, Ben supported the Integrity Assurance element of the Integrated Vehicle Health Management (IVHM) project. The Software Health Management element of IVHM was a main focus. Under the Airspace program he briefly participated in the Separation Assurance element of the Next Generation Air Transportation System (NGATS) project.

From October 2007 through April 2008, Ben was the adviser of Dr. Arturo Tejada, a researcher under the NASA Post-doctoral Research Program. Dr. Tejada was studying the problem of modeling and verifying fault detection techniques used in mechanical systems, such as the cantilever-beam model for an aircraft wing.

Recent Activities (2011 - present)

After a hiatus of several years, development on the Hypatheon database capability resumed in 2008 using a new architecture that emphasizes a self-contained, desktop form of the service. The new Hypatheon tool functions as a GUI companion to PVS that implements a search engine and interacts directly with the PVS prover. It allows large collections of PVS theories to be indexed. Users can search for relevant lemmas during a proof and select one for invocation from the displayed results. Hypatheon was released under the NASA Open Source Agreement in 2012.

Under the System-wide Safety and Assurance Technologies (SSAT) project of the Aviation Safety Program, Ben served as the Langley POC for the Software Intensive Systems element. Verification of numerical software and software change management were goals of this element. Also undertaken were technology transfer efforts to help industry and regulators adapt to the introduction of formal methods-based certification evidence as described in the DO-333 supplement to DO-178C. These efforts (performed under contract) included the development of case studies for DO-333 (completed) and investigations on how to qualify formal methods tools (ongoing).

Under the Airspace Operations and Safety Program (AOSP). Ben is serving as Langley's V&V lead on the Safe Autonomous System Operations (SASO) project. This element includes research on assurance of autonomous operation using deductive techniques, verification of numerical software, runtime monitoring and verification, and the human contribution to safety under increasing autonomy.

In recent work, Ben has devised a framework for symbolically evaluating iterative C code using a deductive approach that automatically discovers and proves program properties. Instead of carrying out verification, the method infers detailed program behavior. A prototype implementation using PVS is under development.

Useful Pointers

• Formal Methods Case Studies for DO-333, a contractor report plus downloadable model files (April 2014).
• Hypatheon, a database capability for PVS theories.
• Manip, a package of PVS strategies for arithmetic simplification.
• PVS libraries and strategies maintained by the formal methods team.
• Home page for the NASA Langley formal methods team.
• Main site of the Langley Research Center.