Optimization of Lyapunov Invariants in Verification of Software Systems
| Autor: | Alexandre Megretski, Mardavij Roozbehani, Eric Feron |
|---|---|
| Přispěvatelé: | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology. Laboratory for Information and Decision Systems, Roozbehani, Mardavij, Megretski, Alexandre |
| Rok vydání: | 2013 |
| Předmět: |
Lyapunov function
Mathematical optimization Optimization problem business.industry Lyapunov optimization Systems and Control (eess.SY) Computer Science Applications symbols.namesake Software Optimization and Control (math.OC) Control and Systems Engineering Control theory Convex optimization FOS: Electrical engineering electronic engineering information engineering FOS: Mathematics symbols Computer Science - Systems and Control Software system Electrical and Electronic Engineering business Lyapunov redesign Mathematics - Optimization and Control Software verification Mathematics |
| Zdroj: | arXiv |
| ISSN: | 1558-2523 0018-9286 |
| DOI: | 10.1109/tac.2013.2241472 |
| Popis: | The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, absence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-analogous to those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification. National Science Foundation (U.S.) (Grant CNS-1135955) National Science Foundation (U.S.) (Grant CPS-1135843) United States. Army Research Office. Multidisciplinary University Research Initiative (Award W911NF-11-1-0046) United States. National Aeronautics and Space Administration (Grant/Cooperative Agreement NNX12AM52A) |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|