For two Kansas State University professors, receiving one of software engineering's most prestigious awards was more than 10 years in the making.
A seven-member research team that included K-State's John Hatcliff, professor of computer and information science, and Robby, associate professor of computing and information science, set out in 1998 to illustrate how different technologies could test for problems that arise when computer programs multitask. The team published 'Bandera: Extracting Finite-State Models from Java Source code' in 2000.
The publication recently received the Most Influential Paper Award from the International Conference on Software Engineering, the world's largest academic software engineering conference. The award honours the publication that has the biggest influence on the theory and practice of software engineering in the 10 years since it was published.
'Our main contribution was to illustrate how model checking, a technique based on discrete mathematics and formal logic, could be applied to software systems to reason about systems that were multitasking in nature,' Hatcliff said. 'Because it provides systematic reasoning about a computer system, model checking can uncover bugs that were hard to detect using existing techniques, such as conventional testing and manual source code inspections.'
Other members of Hatcliff and Robby's research team included: James Corbett, a faculty member at the University of Hawaii at the time of writing and now a Google employee; Matthew Dwyer, a K-State faculty member at the time and now a faculty member at the University of Nebraska-Lincoln; Shawn Laubach, a K-State graduate student at the time; Corina Pasareanu, a K-State doctoral student at the time who now works at NASA; and Hongjun Zheng, a K-State postdoctoral student at the time of writing.
Academic citations show the continuing influence of the team's work. The publication is the most-cited paper published in the 30-year conference history, and the second most-cited of more than 10,000 papers published by the Association of Computing Machinery's SIGSOFT, the leading professional software engineering association. The Google Scholar citation index says the paper currently has more than 800 citations.
'What was interesting about this project was that it brought together a number of different technologies, and that was really one of the things that made this paper stand out,' Robby said.
The project idea developed in the 1990s with the proliferation of the embedded system. As computer software was able to multitask, it became more difficult to test and predict errors. The researchers wanted to develop a way to foresee a program's behaviour, so they applied a technique called model checking, which had been used by hardware engineers to explore how computer chips could execute tasks.
'To get model checking to work for software, we had to develop a lot of sophisticated techniques that automatically discover important properties of a system's source code,' Hatcliff said. 'The goal of these techniques was to boil all the complex features of software down to a relatively clean mathematical model that we can analyse with model checking technology.'
Since the researchers published their work, organisations such as Microsoft and NASA have built off of it, and other groups are working to better design concurrent programming and to build software in different ways. When NASA's Java Path Finder model checking project received NASA's prestigious Turning Goals Into Reality award in 2003, the K-State researchers were listed as members of the project because of the influential contributions and collaboration from their 2000 publication. Pasareanu now leads the Java Path Finder project at NASA.