loader image

Test Solutions for Simulink Models & Production Code

产品

BTC 形式测试套件

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

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

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

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

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

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

直观的图形语言

通用的模板

从我们的角度来看,形式符号在嵌入式开发项目中没有得到更多的接受,主要有两个原因:
像LTL这样的形式语言通常被认为太难使用
它们没有为现有的非形式需求提供足够的可追溯性。
使用通用模板,我们可以有效地解决这两个问题。图形表示既可用作编辑器,又可用作文档,使形式化需求易于创建、理解和审查。我们可以称之为“基于模型的需求工程”。 典型的形式化工作流程从导入现有自然语言要求开始。直观的用户界面通过三个主要步骤引导您完成形式化过程:
Group
第一步,将需求中的单个表达式或事件标识为所谓的“宏”。
Group Copy 2
在第二步中,这些宏以图形方式构建以定义它们的关系和时序行为。
Group Copy 3
在最后一个工作流步骤中,宏被映射到被测系统的真实接口对象,使需求形式化且机器可读。

最后一个有意义的定义

需求覆盖度

对于自然语言需求,需求覆盖的定义总是一个棘手的问题。我们如何确定一个测试用例真正涵盖了它的相关需求?我们如何确定一个测试用例足以完全满足需求? 这些问题的答案通常依赖于人工审查。
基于通用模式规范方法,我们为需求覆盖率提供了有意义且数学上合理的定义。对于一组给定的测试用例,将自动评估和报告此覆盖率。在覆盖范围不完整的情况下,您甚至可以完全自动生成缺失的测试用例。

100%自动化

形式化需求=更好的质量

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

形式测试

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

自动生成测试用例

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

形式验证

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

certified

ISO 26262

BTC EmbeddedPlatform (incl. BTC EmbeddedTester BASE, BTC EmbeddedTester, BTC EmbeddedSpecifier and BTC EmbeddedValidator) has been certified by German TÜV Süd as fit for usage in safety critical software development projects.

The certificate addresses different standards including ISO 26262, IEC 61508-3:2010, ISO 25119, IEC 62304 as well as EN 50716.

For the automotive standard ISO 26262, we have been certified with the highest tool confidence level TCL and the certificate is valid for all ASIL levels including ASIL D.

We provide the certificate and the corresponding report to our customers free of charge upon request, which almost eliminates any effort for tool qualification measures on the customer side.

ISO 26262 Certificate

申请试用License

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

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

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

申请试用license

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

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

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

BTC EMBEDDED SYSTEMS BLOG

来自我们的Blog

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

产品视频

视频

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

BTC 形式验证套件

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