• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle.
【24h】

Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle.

机译：嵌入式控制系统设计和验证的正式方法：应用于自动驾驶汽车。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The design of reliable embedded control systems inherits the difficulties involved in designing both control systems and distributed (concurrent) computing systems. Design bugs in these systems may arise from the unforeseen interactions among the computing, communication and control subsystems. Motivated by the difficulties of finding this type of design bugs, this thesis develops mathematical frameworks, based on formal methods, to facilitate the design and analysis of such embedded systems. An expressive specification language of linear temporal logic (LTL) is used to specify the desired system properties. The practicality of the proposed frameworks is demonstrated through autonomous vehicle case studies and autonomous urban driving problems.;Our approach incorporates methodology from computer science and control, including model checking, theorem proving, synthesis of digital designs, reachability analysis, Lyapunov-type methods and receding horizon control. This thesis consists of two complementary parts, namely, verification and design. First, we introduce Periodically Controlled Hybrid Automata (PCHA), a subclass of hybrid automata that abstractly captures a common design pattern in embedded control systems. New sufficient conditions that exploit the structure of PCHAs in order to simplify their invariant verification are presented.;Although the aforementioned technique simplifies an invariant verification of PCHAs, finding a proper invariant remains a challenging problem. To complement the verification efforts, in the second part of the thesis, we present a methodology for automatic synthesis of embedded control software that provides a formal guarantee of system correctness, with respect to its desired properties expressed in linear temporal logic. The correctness of the system is guaranteed even in the presence of an adversary (typically arising from changes in the environments), disturbances and modeling errors. A receding horizon framework is proposed to alleviate the associated computational complexity of LTL synthesis. The effectiveness of this framework is demonstrated through the autonomous urban driving problems.
机译：可靠的嵌入式控制系统的设计继承了设计控制系统和分布式（并行）计算系统所涉及的困难。这些系统中的设计错误可能源于计算，通信和控制子系统之间不可预见的相互作用。由于发现此类设计错误的困难，本论文基于形式化方法开发了数学框架，以促进此类嵌入式系统的设计和分析。线性时间逻辑（LTL）的一种表达规范语言用于指定所需的系统属性。通过自动驾驶汽车案例研究和自动驾驶城市驾驶问题证明了所提出框架的实用性。;我们的方法融合了计算机科学和控制学的方法论，包括模型检查，定理证明，数字设计综合，可达性分析，Lyapunov型方法和后退的地平线控制。本文由验证和设计两个互补部分组成。首先，我们介绍周期控制混合自动机（PCHA），它是混合自动机的子类，可以抽象地捕获嵌入式控制系统中的通用设计模式。提出了利用PCHA的结构以简化其不变性验证的新的充分条件。尽管上述技术简化了PCHA的不变性验证，但是找到合适的不变性仍然是一个具有挑战性的问题。为了补充验证工作，在论文的第二部分中，我们提出了一种自动综合嵌入式控制软件的方法，该方法相对于线性时间逻辑表示的所需属性，为系统正确性提供了形式上的保证。即使存在对手（通常由环境变化引起），干扰和建模错误，也可以保证系统的正确性。提出了后退的框架以减轻LTL综合的相关计算复杂性。通过自动驾驶城市问题证明了该框架的有效性。

著录项

  • 作者

    Wongpiromsarn, Tichakorn.;

  • 作者单位

    California Institute of Technology.;

  • 授予单位 California Institute of Technology.;
  • 学科 Engineering Automotive.;Engineering Robotics.;Engineering Mechanical.
  • 学位 Ph.D.
  • 年度 2010
  • 页码 169 p.
  • 总页数 169
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号