首页> 外文期刊>Automated software engineering >Automated verification of code automatically generated from Simulink~®
【24h】

Automated verification of code automatically generated from Simulink~®

机译:从Simulink〜®自动生成的代码的自动验证

获取原文
获取原文并翻译 | 示例

摘要

The CLawZ toolset independently and automatically proves the correctness of code automatically generated by a commercial auto-code generator for the Simulink~® modelling language. The use of formal methods is invisible to the user and it has been shown to lead to faster development of correct code. The CLawZ toolset has been continually developed and used for over a decade to prove the correctness of embedded real time safety critical software for Eurofighter Typhoon. The only requirement on the commercial auto-coder is that it provides traceability information between the signal wires in a Simulink~® model and the program variables that implement them.
机译:CLawZ工具集可以独立地自动证明由商用自动代码生成器针对Simulink〜®建模语言自动生成的代码的正确性。形式化方法的使用对于用户是不可见的,并且已证明可导致更快地开发正确的代码。 CLawZ工具集已经持续开发并使用了十多年,以证明Eurofighter Typhoon嵌入式实时安全关键软件的正确性。商用自动编码器的唯一要求是,它可以在Simulink®模型中的信号线与实现它们的程序变量之间提供可追溯性信息。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号