loader image

Test Solutions for Simulink Models & Production Code

Use Cases
Supported Environments
Products
Products

Test Solutions for Simulink Models & Production Code

Use Cases
Supported Environments
Products

产品

BTC 形式验证套件

安全关键系统的证明能力

100% 数学完整性

超越测试

BTC 形式验证套件 是一种正式验证安全关键要求的工具。 在现代嵌入式开发项目中，输入信号和校准的可能值组合的数量很容易爆炸到无穷大。即使有大量的测试用例，也无法通过软件逻辑覆盖所有潜在路径。换句话说，即使经过严格测试，一个非常重要的问题仍然没有得到解答：“我的安全要求会被违反吗？” BTC 形式验证套件使用模型检查技术自动证明您的软件不能违反给定的要求。换句话说——没有任何输入信号和校准值的组合可以将系统驱动到我们感兴趣的不安全状态。
info (3)

模型检查

BTC Embedded Systems 率先将模型检查技术与商业软件工具相结合。向行业专业人士提供这种高度自动化的技术可帮助我们的客户显着提高嵌入式开发项目的效率和质量。 模型检查器的目的是针对特定时间属性广泛分析系统行为，以自动确定该属性是否成立。如果不成立，模型检查器会返回一个具体的反例，明确显示如何违反相应的属性。与传统测试相比，模型检查器只需按一下按钮即可分析系统所有可能的运行，并提供系统动态行为的完整数学证明。反例的生成将模型检查与其他自动分析方法（例如抽象解释）区分开来。

智能且强大

调试

如果 BTC 形式验证套件确实生成了反例表明我们的系统违反了我们的安全要求，您可以使用 BTC EmbeddedPlatform 强大的调试功能自动创建调试环境并跟踪问题。

在开发这个工作流程时，我们问自己：一个好的调试环境是什么样的？

  1. 由于调试通常是一个迭代和试验过程，它应该在模型的新的、独立的副本上完成，而不是在原始模型上。
  2. 由于用户经常希望与同事共享他们的调试环境，因此应该很容易创建调试环境，而无需任何工具链依赖项
对于基于模型的开发过程，最直观的调试环境显然是 Simulink 模型。 BTC 形式验证套件将调试环境生成为独立的沙箱，便于与同事或客户共享。为了更深入地了解代码级别的行为，还可以将调试环境导出为 Microsoft Visual Studio 项目或任何其他 IDE 的通用调试环境。

认证

ISO 26262

BTC 形式验证套件（BTC EmbeddedPlatform 的一部分）已获得德国 TÜV Süd 的认证，适用于安全关键软件开发项目。 该证书适用于不同的标准，包括 IEC 61508-3:3010、ISO 26262、EN 50128、IEC 62304 以及 ISO 25119。对于汽车标准 ISO 26262，该证书适用于所有 ASIL 级别，包括 ASIL D。作为验证工具, BTC Back-to-Back测试套件已被列为 TCL 3 的最高工具置信度等级。 我们根据客户的要求免费提供证书和相应的报告，这大大减少甚至消除了客户方进行工具鉴定措施的任何努力。
Group 6 了解更多
ISO 26262 Certificate

申请试用License

如果您想试用我们的工具，我们很乐意免费提供评试用License。评估包括免费的发布研讨会，还为您提供了与我们的支持和工程团队进行一对一会面的机会。

Group 6 申请License

预定与我们的工程团队的会议

您有任何问题或希望看到我们的工具在实际项目中运行吗？如果是这样，请使用下面的链接安排会议，我们的工程团队成员将很乐意向您展示功能和用例，并直接回答您可能遇到的任何问题。

Group 26 预定会议

申请试用license

如果您想试用我们的工具，我们很乐意免费提供评试用License。评估包括免费的发布研讨会，还为您提供了与我们的支持和工程团队进行一对一会面的机会。
Group 6 申请 License

预定与我们的工程团队的会议

您有任何问题或希望看到我们的工具在实际项目中运行吗？如果是这样，请使用下面的链接安排会议，我们的工程团队成员将很乐意向您展示功能和用例，并直接回答您可能遇到的任何问题。

Group 26 预定会议

BTC EMBEDDED SYSTEMS BLOG

来自我们的Blog

分享有关嵌入式软件开发、基于模型的设计、自动代码生成和符合 ISO 26262 的测试的见解。
Blog

Interview: How does a Model Checker work?

  • Automotive software covers more and more safety critical features and challenges testing to provide good confidence of the software
  • Model Checkers are used in various testing use cases, but what are they good for?
  • This article describes the approach and advantages as well as limitations of model checking in testing.
Read more

Wolfgang Meincke

Stuttgart, Germany

Blog

The Power of Focus – How to Optimize a Model Checker for Embedded Software

  • Model checking is a powerful technique to analyze the dynamic behavior of software with mathematical completeness
  • The complexity of the algorithm makes it challenging to apply model checking to industrial applications
  • In this article, our Chief Research Engineer shares some insights into how BTC has addressed these challenges
Read more

Dr. Tino Teige

Oldenburg, Germany

产品视频、视频博客和网络研讨会

视频&网络研讨会

在这些短视频中了解我们产品的一些主要功能。
Play now
FormalVerification_Start-1
播放视频
Play now
FormalVerification_Start-1
播放视频
Play now
FormalSpecification-1
播放视频
Play now
FormalSpecification-1
播放视频

BTC 功能测试套件

针对 Simulink、TargetLink、Embedded Coder和手写代码的基于需求的测试。
详细信息

我们提供智能和自动化的测试解决方案，使我们的客户能够处理日益复杂的嵌入式软件，同时实现符合ISO 26262标准的高质量。

产品
公司
新闻
知识库
联系
Youtube Linkedin
产品
公司
新闻
知识库
联系
Youtube Linkedin

Copyright © 2025 BTC Embedded Systems