User-Interfaces for Formal Methods Systems

With SBIR support from ONR, GrammaTech is working to improve the quality and reliability of software by speeding the adoption of formal methods in industry.

Development of strategic software infrastructure aimed at overcoming these obstacles:

Investment Catch-22. Small markets discourage investment, resulting in poor tools; poor tools discourage adoption.
Industry Resistance. Industry is reluctant to adopt new tools and processes, especially esoteric ones with high educational prerequisites.
Researcher Isolation. Most formal methods researchers are too remote from industrial practice.
Tool Isolation. Valuable formal methods are locked inside researcher’s monolithic prototypes.
User-Interface Inadequacies. Most formal methods prototypes have weak idiosyncratic user interfaces.

GrammaTech's approaches to overcoming these obstacles are:

Build infrastructure for a Formal Methods Environment (FME) tightly integrated with an established industrial analysis and design environment.
Address the Investment Catch-22 by capitalizing on the significant existing investment in CASE tools.
Ameliorate Industrial Resistance by building the FME within an environment industry has already embraced.
Overcome Researcher Isolation from industrial practice by getting researchers to use the FME for their prototypes.
Tackle Tool Isolation by adopting industry standard component technology, thereby enabling integration of diverse formal methods tools within the common FME framework.
Address User-Interface Inadequacies with a Formal Methods Interface (FMI) toolkit incorporated as part of the FME.
Develop both graphical user-interfaces (GUIs) and application programmer interfaces (APIs) for a common intermediate representation that can be shared by multiple formal methods applications.

The common intermediate representation of the Toolkit is based on system dependence graphs (SDGs). SDGs are a semantically rich representation that describes programs in terms of their deep structural properties. In contrast, abstract syntax trees are mere surface structure. SDGs deliver the results of sophisticated static analyses in a form that substantially raises the level of discourse for the subsequent analyses, transformations, and compositions needed by formal methods. Thus, they have a far greater potential as a common intermediate representation for the FME than attributed abstract syntax trees.