In today’s world, individuals, society, and nations all depend on software to manage critical infrastructures for power, banking and finance, air traffic control, telecommunications, transportation, national defense, and healthcare. Dr. Hridesh Rajan, at Iowa State University (ISU)’s Department of Computer Science, along with Dr. Tien Nguyen (ISU), Dr. Robert Dyer (Bowling Green State University), Dr. Gary T. Leavens (University of Central Florida), and Dr. Vasant G. Honavar (Penn State University) is launching a NSF project to improve quality of such critical infrastructures by increasing the availability of formal specifications that are used to verify their software. This large "Big Data” collaborative research project has recently been awarded a total of $1,604,843 by the National Science Foundation.
Specifications are critical for communicating the intended behavior of software systems to software developers and users and to make it possible for automated tools to verify whether a given piece of software indeed behaves as intended. Safety critical applications have traditionally enjoyed the benefits of such specifications, but at a great cost. Because producing useful, non-trivial specifications from scratch is too hard, time consuming, and requires expertise that is not broadly available, such specifications are largely unavailable. The lack of specifications for core libraries and widely used frameworks makes specifying applications that use them even more difficult. The absence of precise, comprehensible, and efficiently verifiable specifications is a major hurdle to developing software systems that are reliable, secure, and easy to maintain and reuse.
“In other words, when building computer software systems, we have to be certain they are performing the tasks we created them to carry out. To check this, we must have a specific model of what that software is intended to do. This allows us to verify that the software is operating correctly,” offers Dr. Hridesh Rajan. “Other reasons for developing affordable tools and methods are to help us locate errors within the software when we get undesired results, so they may be corrected, in addition to detecting and protecting against unwanted intrusions into our computer systems.”
By leveraging data and collective community expertise, the project will be able to combine analytics over large open source code repositories to augment and improve program analysis-based specification inference through synergistic advances across both these areas. The absence of precise, comprehensible, and efficiently verifiable specifications is a major hurdle to developing software systems that are reliable, secure, and easy to maintain and reuse. The project lends itself to critical advances in big data enabled software engineering.
This multi-university project is being led by ISU, the College of Liberal Arts & Sciences, and the Department of Computer Science. The PI, Dr. Hridesh Rajan, may be contacted for further questions at hridesh@iastate.edu.
For more information on this grant, please see: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1518897