Benedetto L. Di Vito

B.DiVito@NASA.GOV

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 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. In a more service-oriented role, Ben participated on NASA's Software Engineering Research Infusion team.

Beginning in 2006, Ben has been supporting NASA's Exploration Systems Mission Directorate. In the first role, he is a member of the Systems Engineering and Integration team on the Constellation Program, where he has been helping to refine the program-level requirements. In the second role, he is a technical lead on the Spacecraft Autonomy for Vehicles and Habitats project, which is a research effort under the Exploration Technology Development Program.

In earlier years, he 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.

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.

Background

• Education and Experience
• Publications and External Activities

Recent Efforts

In his current assignment with the Safety-Critical Avionics Systems Branch of the Research and Technology Directorate, Ben has been engaged in a variety of Langley research activities. One such topic is the partitioning problem for integrated modular avionics (IMA). His 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. The FAA anticipates a growing need to certify integrated avionics configurations.

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.

Ongoing activities are focusing on the development of new prover strategies to automate aspects of theorem proving for continuous mathematics. In 2002 Ben developed a set of algebraic manipulation strategies called Manip, which may be retrieved from the PVS libraries and strategies page maintained by the formal methods team. Important new features were added to Manip in 2005.

A newer research project initiated by Ben concerns the establishment of a mathematical database service called Hypatheon. This service uses a relational DMBS and supporting tool infrastructure to collect and disseminate PVS theories. Hypatheon will implement various forms of search as well as provide a client module usable along side the PVS prover. Users will be able to conduct searches and download new theories during active prover sessions.

In 2003 and 2005, 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 is 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.

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.

Useful Pointers

• Manip, a package of PVS strategies for arithmetic simplification.
• PVS libraries and strategies maintained by the formal methods team.
• STRATA 2003, the First International Workshop on the Design and Application of Strategies/Tactics in Higher Order Logics
• Lfm2000, the NASA Langley Formal Methods Workshop
• Home page for the NASA Langley formal methods team.
• Main site of the Langley Research Center.