用椭球域分析控制系统软件
Using Ellipsoidal Domains to Analyze Control Systems Software
摘要：
我们提出了一种基于动态系统的控制器安全性能自动验证的方法，例如通常用于航空电子设备的控制器。特别是，我们的重点是证明软件实现线性和一些非线性控制器的稳定性。我们开发了一个抽象的解释框架，紧接着在模型级的证明中使用的李雅普诺夫方法，并描述相应的抽象域，其中线性系统的椭球约束。这些椭圆域提供了状态变量值的抽象，并且必须与对程序中的其余变量进行建模的其他域相结合。因此，自动为每个变量分配正确类型的抽象域的问题出现了。我们提供了一个算法，解决了这个分类问题，在许多实际情况下，并建议如何将其推广到更复杂的情况。然后，我们通过求解矩阵方程找到一个不动点，在线性情况下，这只是离散的李雅普诺夫方程。与软件分析中的大多数情况相反，这个不动点不能通过通常的传播约束的迭代法达到饱和，因此数值方法变得必不可少。最后，我们用几个例子来说明我们的方法。
英文摘要：
We propose a methodology for the automatic verification of safety properties of controllers based on dynamical systems, such as those typically used in avionics. In particular, our focus is on proving stability properties of software implementing linear and some non-linear controllers. We develop an abstract interpretation framework that follows closely the Lyapunov methods used in proofs at the model level and describe the corresponding abstract domains, which for linear systems consist of ellipsoidal constraints. These ellipsoidal domains provide abstractions for the values of state variables and must be combined with other domains that model the remaining variables in a program. Thus, the problem of automatically assigning the right type of abstract domain to each variable arises. We provide an algorithm that solves this classification problem in many practical cases and suggest how it could be generalized to more complicated cases. We then find a fixpoint by solving a matrix equation, which in the linear case is just the discrete Lyapunov equation. Contrary to most cases in software analysis, this fixpoint cannot be reached by the usual iterative method of propagating constraints until saturation and so numerical methods become essential. Finally, we illustrate our methodology with several examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
