Computer scientist helps verify new satellite communication rules

System F6 is the U.S. Defense Department's shorthand designation for a planned staging of multiple mini-satellites, wirelessly connected as they orbit Earth, working in unison to do jobs now performed by single, large satellites.

Networked satellites have advantages of cost, effectiveness and security over traditional single satellites. But turning the concept into reality poses high-level challenges for the scientists and engineers developing it.

Lenore Zuck, UIC associate professor of computer science, is among the scientists tackling the problems. Zuck is a principal investigator along with University of Pittsburgh computer scientists Daniel Mossé and Adam Lee in a Defense Advanced Research Projects Agency, or DARPA-funded project to verify protocols or rules the F6 satellites will use to communicate effectively.

Zuck is focusing on developing the protocol verification framework that makes sure arbitrary configurations of small satellites automatically check for proper connections and faults, efficient power and memory use, and communication privacy.

"Protocols are the core of a communication system, so it's vital to guarantee that they are correct," said Zuck. "Even small software errors may have severe, adverse consequences. And it is costly -- if not impossible -- to fix some errors after the satellites are deployed."

The F6 clusters will use anywhere from four to 20 or more satellites operating in a real-time exchange of information, responding immediately to various inputs.

Because the satellites in the clusters will have so many operating components, verifying the protocols is extremely complicated and will need to be done using special automated software.

"UIC is leading the verification effort and will provide automatic proofs and methodologies to verify the correctness of the protocols," she said.

"You perform formal verification in the design phase. After you go from design to implementation, you try to prove as much as possible that your implementation follows the design. But you should also test it. Formal verification is really good for catching flaws early on," Zuck said. "That's proven itself time and again."

System F6 -- which stands for "Future, Fast, Flexible, Free-Flying Spacecraft United by Information Exchange" -- hopes to begin in-orbit demonstrations of the wirelessly connected satellite modules between 2014 and 2015. The module clusters should function like a single, monolithic satellite, but perform discrete functions, making it a more adaptable and survivable model.

While the study of verification techniques is largely theoretical, Zuck is an adherent of what she calls the "movement for useable verification."

The F6 verification protocols may have application to other aerospace projects. Previous work she did found its way into development of more reliable and versatile products by some of the world's leading high-tech companies.

"I'm a theoretician by training, but I always have an eye on what's applicable," she said. "I like to develop theory that leads to things that are actually useful."

Provided by University of Illinois at Chicago