SHF: Small: Beyond Behavioral Software Contracts

To create complex applications, software developers compose components in a Lego-like manner. Some software systems consist of 100s of components. The interactions among these components are quite intricate, with each individual component relying on informal descriptions on how to use it properly, say, ``always run this functionality before this one, followed by one of these pieces.'' But, if a developer accidentally causes a violation of such descriptions, things can go horribly wrong, leaving the developer team dumbfounded about the cause of the problem.

The investigator and his team are studying novel techniques for automatically turning these informal descriptions into checks. If things go wrong, such checks immediately signal a problem, including hints as to which components are involved in the usage violation. The project will impact the lives of working programmers, eliminating hours of endless search for errors.

The project's goals differ from those of two other approaches that tackle this composition problem. First, type systems check for potential errors before the application is deployed; but existing type systems lack the power to deal with many parts of these informal descriptions. Second, run-time verification monitors complete systems specifications in parallel with the execution of the application; but run-time verification specifications are formulated after the components are linked, meaning the developers of components cannot protect their individual code.

The novelty of this project is to build on, and extend, behavioral software contracts. Instead of checking individual function calls, however, the investigator's team is developing a mechanism for representing sequences of such calls and all values associated with these calls. This mechanism then allows component developers to express informal descriptions in terms of predicates over these sequences.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.