Improving the Applicability of Haskell-hosted Semi-Formal Models to High Assurance Development
Project Award Date: 08-01-2011
Software engineering, at its heart, is about making compromises between the overall efficiency of an implementation and the clarity, agility, and maintainability of the code base. This abstraction gap between intent and practice is especially acute during the development of high-assurance or high performance software systems. ITTC researchers will develop high-level models and efficient implementations concurrently under a single, semi-formal framework that bridges the abstraction gap with aggressive, user-assisted program refinement technology.
The functional language Haskell has enjoyed considerable success as a platform for high-level modeling of complex systems with its mathematical-style syntax, state-of-the-art type system, and powerful abstraction mechanisms. With careful handling, these powerful facilities can be used to express computational concerns in a manner that allows highly specific and efficient implementations of software and hardware. The same language can be used to express a semi-formal model and an efficient implementation, taking the form of two distinct expressions of computation with the same mathematical basis. ITTC researchers will take advantage of this common mathematical foundation and build infrastructure that allows an implementer to construct a user-configurable refinement pipeline between the model and implementation. The two programs can be developed concurrently, and properties of one to be used in the other.
The ability to link a semi-formal model to a concrete implementation brings many benefits
First, the specific elements and contents of the refinement pipeline that link the two programs become precise documentation of the compromises made in the real implementation. Second, starting with the identity pipeline, a model can be aggressively rewritten into an efficient form, with the refinement pipeline being incrementally improved as the form and specifics of the implementation are refactored over time. Third, retrospectively-added changes to the model can be rigorously propagated through the pipeline, requiring the appropriate aspects of the implementation, or the pipeline itself, to be updated, depending on the circumstances.
Faculty Investigator(s): Andrew Gill (PI)
Student Investigator(s): Michael Tabone, , Adam Howell, Andrew Farmer, Nicholas Shaheed, Brad Torrence, James Stanton, Aleksander Eskilson, David Young, Ryan Scott
Primary Sponsor(s): NSF