Products

产品

BTC 形式测试套件

直观的将安全关键需求形式化

轻松步入形式化方法的世界

如果您的计算机能够了解您的要求会怎样？

BTC 形式测试套件允许您为安全关键型项目创建和管理半形式和形式化需求。虽然在ISO 26262和IEC 61508等标准中建议使用半形式和形式化的需求表示法，但阅读和编写大多数形式化表示法语言需要高水平的专业知识。BTC 形式测试套件为您提供了一种直观的图形方法，可以在没有专业知识的情况下从自然语言中得出全面的形式化需求。为您提供了一种直观的图形方法，可以在没有专业知识的情况下从自然语言中得出全面的形式化需求。

形式化的需求 = 更好的需求

在当今的大多数开发项目中，需求都是使用非形式化的自然语言创建和管理的。由于自然语言通常为解释留出一些空间，因此函数开发人员或测试工程师最终可能会实现与预期不同的行为。通过BTC 形式测试套件中的半形式或形式化表示法，您可以将安全要求转换为清晰，明确和机器可读的表示形式 – 提高其质量并使其在开发工作流程的以下步骤中更有价值。

直观的图形语言

通用的模板

从我们的角度来看，形式符号在嵌入式开发项目中没有得到更多的接受，主要有两个原因：

像LTL这样的形式语言通常被认为太难使用

它们没有为现有的非形式需求提供足够的可追溯性。

使用通用模板，我们可以有效地解决这两个问题。图形表示既可用作编辑器，又可用作文档，使形式化需求易于创建、理解和审查。我们可以称之为“基于模型的需求工程”。典型的形式化工作流程从导入现有自然语言要求开始。直观的用户界面通过三个主要步骤引导您完成形式化过程：

第一步，将需求中的单个表达式或事件标识为所谓的“宏”。

在第二步中，这些宏以图形方式构建以定义它们的关系和时序行为。

在最后一个工作流步骤中，宏被映射到被测系统的真实接口对象，使需求形式化且机器可读。

最后一个有意义的定义

需求覆盖度

对于自然语言需求，需求覆盖的定义总是一个棘手的问题。我们如何确定一个测试用例真正涵盖了它的相关需求？我们如何确定一个测试用例足以完全满足需求？这些问题的答案通常依赖于人工审查。

基于通用模式规范方法，我们为需求覆盖率提供了有意义且数学上合理的定义。对于一组给定的测试用例，将自动评估和报告此覆盖率。在覆盖范围不完整的情况下，您甚至可以完全自动生成缺失的测试用例。

100%自动化

形式化需求=更好的质量

由于形式化需求的机器可读性，您可以在多个验证用例中直接使用它们，并显着提高验证过程的质量和完整性：

形式测试

在传统的基于需求的测试过程中，每个测试用例仅根据派生自的需求进行评估。但是，如果测试用例 N°5 违反了要求 N°10 呢？形式测试根据所有形式化需求对所有测试用例执行自动交叉检查。这使您可以检测其他影响，而无需任何额外的测试工作。

自动生成测试用例

如果现有测试用例未完全满足特定形式要求，则基于需求的测试生成附加组件允许自动生成缺失的测试用例，从而为所有需求提供 100% 的覆盖率。

形式验证

借助我们强大的模型检查技术，可以自动获得数学上完整的证明，从而保证您的软件实现永远不会违反安全需求。如果可能违反需求，我们会以测试用例的形式生成反例。

认证

ISO 26262

BTC EmbeddedPlatform已通过德国TÜV Süd认证，适合用于安全关键软件开发项目。该证书适用于不同的标准，包括IEC 61508-3：3010，ISO 26262，EN 50128，IEC 62304以及ISO 25119。对于汽车标准ISO 26262，该证书适用于所有ASIL级别，包括ASIL D。作为验证工具，BTC EmbeddedTester被归类为TCL 3的最高工具置信度。我们根据要求免费向客户提供证书和相应的报告，这大大减少甚至消除了客户方工具认证措施的任何努力

申请试用License

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

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

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

申请试用license

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

BTC EMBEDDED SYSTEMS BLOG

来自我们的Blog

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

Blog

5 1 月, 2021

Why and How to Improve Requirements

Requirements stand at the beginning of each development process and their quality has an impact on all following steps
The quality of requirements in embedded software projects is often insufficient
This article shows how formalization can help to increase the requirements quality

Wolfgang Meincke

Stuttgart, Germany

产品视频

视频

在这些短视频中了解我们产品的一些主要功能。

Play now

BTC 形式验证套件

安全关键型系统的证明能力

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

Test Solutions for Simulink Models & Production Code

Use Cases

Supported Environments

Products

Test Solutions for Simulink Models & Production Code

Use Cases

Supported Environments

Products

产品

BTC 形式测试套件

轻松步入形式化方法的世界

如果您的计算机能够了解您的要求会怎样？

形式化的需求 = 更好的需求

直观的图形语言

通用的模板

最后一个有意义的定义

需求覆盖度

100%自动化

形式化需求=更好的质量

形式测试

自动生成测试用例

形式验证

认证

ISO 26262

申请试用License

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

申请试用license

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

BTC EMBEDDED SYSTEMS BLOG

来自我们的Blog

Why and How to Improve Requirements

产品视频

视频

BTC 形式验证套件

产品

公司

新闻

知识库

联系

产品

公司

新闻

知识库

联系