Communications of the ACM
Can Control Theory Make Software Better?
The oscillation of a pendulum offers the simplest example of a Lyapunov function, a central concept in control theory. The pendulum's loss of energy with each swing guarantees that it won't lurch into a less-stable state.
Credit: MIT News
Researchers at the Massachusetts Institute of Technology and Georgia Tech recently demonstrated the application of control theory principles to formal verification, in a method that could benefit approximate computation.
The researchers adapted the Lyapunov function used in control theory, which has a standard graph that slopes everywhere toward its minimum value. If the Lyapunov function represents a physical system's dynamics and the minimum value depicts a stable state, then the curve of the graph guarantees the system will move toward increased stability.
The researchers imagine a computer program as a set of rules for navigating a space defined by the program's variables and the program instructions' memory locations, with execution problems such as overloading the memory being regions in the space. Formal verification then requires proof that the program's variables will never reach danger zones.
The researchers believe their method will be effective at least for control-system software and that it has possible applications in approximate computation.
"This is the first work that is formalizing the notion of robustness for software," says University of Pennsylvania's George Pappas. "It’s a paradigm shift...to a view where you try to see how robust your software is to changes in the input or the internal state of computation."
From MIT News
View Full Article
Abstracts Copyright © 2013 Information Inc., Bethesda, Maryland, USA
No entries found