NASA Langley Formal Methods



quick page






  home > team > civil servants > bld

Benedetto L. Di Vito

Email: B.DiVito@NASA.GOV


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 fault-tolerant computing and flight-critical avionics. In recent years he investigated methods for automating certain classes of proofs, such as those involving real-valued arithmetic and properties of state machine models. He has also been studying how databases can be used to enhance the effectiveness of interactive proof. He has recently contributed to investigations on assurance techniques for numerically intensive software applications.

Under NASA's Aeronautics Research Mission Directorate, Ben has supported two programs: the Aviation Safety Program and the Airspace Program. In his current assignment for Aviation Safety he is participating in the System-wide Safety and Assurance Technologies (SSAT) project. He is supporting both the Verification and Validation for Flight-Critical Systems (VVFCS) sub-project as well as the Prognostics and Decision Making (PDM) sub-project.

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.

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


Previous 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.

Recent Activities (2005 - present)

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.

After a hiatus of several years, development on Hypatheon 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. As of July 2011, a fairly complete prototype is in use internally. Public release of Hypatheon is expected in December 2012.

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.

For the Verification and Validation for Flight-Critical Systems (VVFCS) sub-project of Aviation Safety, Ben is serving as the Langley POC for the Software Intensive Systems element. Verification of numerical software is a major goal of this element.

Useful Pointers


home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ben L. Di Vito
larc privacy statement
last modified: 29 November 2012