《控制系统软件的形式验证》

本书是控制系统软件分析和验证的重要介绍；

控制系统软件的验证对于许多技术和行业至关重要，从航空和医疗技术到我们驾驶的汽车。控制器软件的故障可能会使人丧生。在这本权威且易于理解的书中，作者Pierre-Loïc Garoche 为控制工程师和计算机科学家提供了分析和验证这一重要软件类别的形式化技术不可或缺的介绍。

很多时候，控制工程师不了解围绕软件验证的问题，而计算机科学家往往不熟悉控制器软件的特殊性。Garoche提供了一种统一的方法，面向这两个领域的研究生，涵盖形式验证方法以及控制器的设计和验证。他介绍了大量新的验证技术，用于对控制器软件进行详尽分析。其中包括计算非线性不变量的新方法，凸优化工具的使用以及处理数值不精确性的方法，例如分析软件中发生的浮点计算。

随着关键系统的自主性不断提高——自动驾驶汽车、无人机、卫星和着陆器证明了这一点——这些系统中的数值功能变得越来越先进。这里介绍的技术对于支持对这些新兴技术中使用的控制器软件进行形式分析至关重要。