ITTC Project

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

Project Sponsors

Primary Sponsor(s): NSF

Partner with ITTC

The Information and Telecommunication Technology Center at the University of Kansas has developed several assistance policies that enhance interactions between the Center and local, Kansas, or national companies. 

ITTC assistance includes initial free consulting (normally one to five hours). If additional support is needed, ITTC will offer one of the following approaches: 

Sponsored Research Agreement

Individuals and organizations can enter into agreements with KUCR/ITTC and provide funds for sponsored research to be performed at ITTC with the assistance of faculty, staff and students.

Licensing and Royalty/Equity Agreement

An ITTC goal is the development of investment-grade technologies for transfer to, and marketing by, local, Kansas, and national businesses. To enhance this process, the Center has developed flexible policies that allow for licensing, royalty, and equity arrangements to meet both the needs of ITTC and the company.

Commercialization Development

Companies with a technology need that can be satisfied with ITTC's resources can look to us for assistance. We can develop a relationship with interested partners that will provide for the development of a technology suited for commercialization.

ITTC Resource Access

ITTC resources, including computers and software systems, may be made available to Kansas companies in accordance with the Center's mission and applicable Regents and University policies.

ITTC Calendar
There are no upcoming events at this time.