无人激进机动汽车控制器的自动化可信自动编码
系统与控制
2013-08-28 v1
摘要
本文描述了可信自动编码框架在控制系统中的应用，以非线性汽车控制器为例。该框架生成代码，并提供关于代码的高级功能属性的保证，这些保证可以被独立验证。这些高级功能属性不仅作为系统良好行为的证书，还可用于保证不存在运行时错误。在我们之前的一项工作中，我们构建了一个带有证明的原型自动编码器，以全自动方式展示了该框架在线性和准非线性控制器上的应用。针对非线性汽车示例，我们提议进一步扩展原型的数据流注释语言环境，引入几个新的注释符号，以启用一般谓词和动力系统的表达。我们手动演示了原型自动编码器的新扩展如何使用输出语言 Matlab 在汽车控制器上工作。最后，我们讨论了对文档化输出代码进行自动分析和验证的要求及可扩展性问题。
引用
@article{arxiv.1308.5964,
title = {Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller},
author = {Timothy Wang and Eric Feron},
journal= {arXiv preprint arXiv:1308.5964},
year = {2013}
}