• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International symposium on model checking of software >A Sample of Formal Verification Research for Embedded Control Software at ONERA
【24h】

A Sample of Formal Verification Research for Embedded Control Software at ONERA

机译：ONERA嵌入式控制软件的形式验证研究样本

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This talk presents a sample of research work conducted by the French Aerospace Lab (ONERA) on tailoring and applying formal methods to advanced embedded controllers, at various phases of the development and verification process, illustrated by industrial projects and collaborations. A first line of work1, carried out in partnership with Airbus, Dassault and LAAS-CNRS, aims at going beyond simulation for validating advanced hybrid control laws, by leveraging bounded reachability analysis and robustness analysis from the early design phases. This requires to bridge the representation gap existing between hybrid dataflow formalisms used to model control laws (e.g. Simulink, Scade-Hybrid,...), and the automata-based formalisms used by most hybrid model-checkers (e.g. SpaceEx, Flow*, dReach,...) and robustness analysis frameworks. We discuss the steps taken to handle the complexity and size of typical industrial models. A second line of work, carried out jointly with academic lab LRI (Paris-Sud, INRIA) and technology provider OcamlPro, addresses the sound combination of SMT-solvers and potentially unsound convex optimization engines to allow proving complex polynomial invariants on advanced control laws implementations. Such implementations are usually obtained by automatic time-discretization and code generation from a hybrid dataflow model. The proposed approach shows a notable performance improvement on controllers of interest with respect to earlier approaches based on interval arithmetic or purely symbolic methods such as cylindrical algebraic decomposition or virtual substitutions. Last, we present research conducted2 in partnership with Liebherr Aerospace Toulouse and technology provider Systerel on leveraging model-checking techniques for unit-level test case generation for an air management system, taking into account the industrial setting and qualification constraints, following DO-178C and D0-333 guidelines.
机译：本演讲提供了法国航空航天实验室（ONERA）进行的研究工作样本，该研究工作涉及在开发和验证过程的各个阶段，将形式化方法应用于高级嵌入式控制器，并将其应用到工业项目和合作中。与空客，达索和LAAS-CNRS合作进行的第一项工作1旨在通过利用早期设计阶段的有限可达性分析和鲁棒性分析，超越模拟来验证先进的混合控制律。这就需要弥合用于建模控制律的混合数据流形式主义（例如Simulink，Scade-Hybrid等）与大多数混合模型检查器使用的基于自动机的形式主义（例如SpaceEx，Flow *， dReach，...）和鲁棒性分析框架。我们讨论了处理典型工业模型的复杂性和规模所采取的步骤。与学术实验室LRI（Paris-Sud，INRIA）和技术提供商OcamlPro联合进行的第二项工作是解决SMT求解器和可能不健全的凸优化引擎的合理组合，以允许在高级控制律实施中证明复杂的多项式不变量。通常通过从混合数据流模型自动进行时间离散化和代码生成来获得此类实现。相对于基于区间算术或纯符号方法（例如圆柱代数分解或虚拟替换）的早期方法，所提出的方法在感兴趣的控制器上显示出显着的性能提升。最后，我们介绍了与利勃海尔图卢兹航空航天公司和技术提供商Systerel合作进行的研究2，该研究利用模型检查技术为空气管理系统生成单元级测试用例，同时考虑了工业设置和资格限制，并遵循DO-178C和D0-333指南。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号