软件系统验证中李雅普诺夫不变量的优化
系统与控制
2011-08-02 v1 最优化与控制
摘要
本文提出了一种用于数值软件系统验证的控制理论框架，并将软件验证作为控制与系统理论的一个重要应用。其思想是将李雅普诺夫函数及相关的计算技术从控制系统分析和凸优化转移到各种软件安全性和性能规范的验证中。这些规范包括但不限于：无溢出、无除零、有限时间终止、死代码存在以及某些用户指定的断言。该框架的核心是李雅普诺夫不变量。这些是程序变量的适当构造的函数，并沿着执行轨迹满足某些类似于李雅普诺夫函数的性质。对这些不变量的搜索可以表述为一个凸优化问题。如果相关的优化问题是可行的，其结果就是该规范的一个证明。
引用
@article{arxiv.1108.0170,
title = {Optimization of Lyapunov Invariants in Verification of Software Systems},
author = {Mardavij Roozbehani and Alexandre Megretski and Eric Feron},
journal= {arXiv preprint arXiv:1108.0170},
year = {2011}
}