10/8/2020 Aaron Seidlitz, Illinois CS
Runtime Verification will use its own K Framework to eliminate strange behaviors and portability issues NASA encounters with programming done in C.
Written by Aaron Seidlitz, Illinois CS
A decade ago, Illinois CS professor Grigore Rosu had a vision for the company he started, called Runtime Verification. He simply wanted to commercialize the technology he developed in his research lab at the university.
As with most new concepts, though, Rosu can recall the early detractors that rejected his research. But, as time passed and his perseverance endured, he began to develop that very same research into published papers and conference discussions.
The company came about shortly after that, and it quickly found its niche in the industry. Success at Runtime Verification came through funded projects with Toyota, NASA, Boeing and the National Science Foundation.
Most recently, Rosu’s Runtime Verification earned funding from NASA’s Small Business Innovation Research (SBIR) program for the third time. This project – titled “A Semantics-Based Verification Toolset for UAS Embedded Software” – has several phases over a period of up to three years and can provide nearly $2 million in grant money in total. Each phase is approved by NASA based on the success of the previous phases.
The primary issue NASA turned to Verification for, Rosu said, stems from inconsistencies in programming with the C language.
“We had two other similar grants with NASA in the past. This time, we want to develop a tool that, first of all, works with mission-critical NASA software. Second, we want to develop a tool that NASA scientists and engineers can and will use. At the same time, this kind of work allows us to continue developing our K technology for future projects,” Rosu said. “I hope that by the end of this project, NASA will start using this technology internally. That would be, to me, the measure of success.”
Although the professor and CEO believes that C is a great language for performance, he also emphasizes that there is a price to pay for that performance – an increased likelihood of strange behaviors.
Runtime Verification’s solution is to apply its K Framework, which is a mathematically rigorous toolset that gives users the ability to design and implement programming languages from basic principles, and derive software analysis tools for them following a correct-by-construction methodology. These factors allow users of the K framework to ultimately verify their programs and systems for maximum assurance.
Further heightening the issues at NASA, according to Rosu, is that C was created with performance and not portability in mind. Indeed, odd behaviors occur when the C program written and heavily tested on one machine is then executed on other machines running on other architectures. NASA encounters this on a daily basis, when their C programs written and tested on desktops or workstations are then deployed on other machines or devices, such as a spacecraft, aircraft, rover or even a car.
This is when Rosu’s K Framework shines.
The essence of Runtime Verification, as described on the company website, is to design “formal models for high-value application domains, then use the models to develop domain-specific products and services focused on correctness and security.”
Runtime Verification now does this primarily through the K Framework.
“That’s how we started the company. We use several other technologies in the company besides the K Framework, but the K Framework is one of our core and unique capabilities. This fuels our activities and passion within the company,” Rosu said.
During the last decade, projects like this one with NASA occurred with enough frequency to encourage organic growth at Runtime Verification based on two primary components.
First, additions to the company happened no more than one or two employees at a time. At this point, Runtime Verification employs about 30 people. Often, Rosu said, academic professionals who start a company receive a surplus of funding tied to lofty production goals right as the company is starting.
This encourages the CEO to hire many new people at once. This often causes teams that lack cohesiveness. Rosu said the consistent approach his company has received through steady but smaller funding opportunities has allowed him to hire the right people at the right time, thus forging a more family-like atmosphere.
Second, that tight-knit staff approach heightened because of who he’s hired— many former UIUC students, including CS graduates with prior knowledge of Rosu and the K Framework.
This has driven a mindset toward accomplishing goals together, which Rosu grew fond of witnessing.
“From the very beginning, I've felt responsible and very proud,” he said. “Our team includes so many smart people, who are, in fact, many former students, about half of whom have advanced degrees from our university.
“I’m very glad and honored that they bought into the vision of our company.”