loader image

针对Simulink模型和量产代码的测试解决方案

针对 ADAS/AD 虚拟验证的挑战

如何创建所需的数百万个方案?

如何避免测试爆炸问题?

如何确定我的测试是通过还是失败?

Products

针对Simulink模型和量产代码的测试解决方案

针对 ADAS/AD 虚拟验证的挑战

如何创建所需的数百万个方案?

如何避免测试爆炸问题?

如何确定我的测试是通过还是失败?

Use Cases

Formal Specification

Intuitive formal specification of safety requirements

Formal Requirements =
Better Requirements

What if your computer could understand your requirements?

In most development projects today, requirements are created and managed using informal natural language. 

As natural language typically leaves some room for interpretation, there’s the possibility that function developers or test engineers ultimately implement a different behavior than intended. 

With a semi-formal or formal notation in BTC EmbeddedSpecifier, you can transform your safety requirements into a clear, unambiguous and machine-readable representation – improving their quality and making them much more valuable for the following steps in the development workflow.

Play now
FormalSpecification-1
播放视频
Play now
FormalSpecification-1
播放视频

Intuitive graphical language

Universal Pattern

From our perspective, formal notations have not gained more acceptance in embedded development projects for two primary reasons:

Formal languages like LTL are often considered to be too difficult to use

They do not provide enough traceability towards existing informal requirements.

With Universal Pattern, we address both issues efficiently. The graphical representation serves as an editor and at the same time as documentation, making the formal requirement easy to create, understand and review. We could call this “Model-based Requirements Engineering”.

A typical formalization workflow starts with the import of existing natural language requirements. The intuitive user interface guides you through the formalization process in three main steps:

Group

In the first step, individual expressions or events within the requirement are identified as so-called “macros.”

Group Copy 2

In a second step, these macros get graphically structured to define their relationship and timing behavior. 

Group Copy 3

In the last workflow step, the macros are mapped to real interface objects of the system-under-test – making the requirement formal and machine-readable.

Finally a meaningful definition

Requirement Coverage

With natural language requirements, the definition of requirement coverage is always a tricky question. How can we be sure that a test case really covers its linked requirement? How can we be sure that one test case is enough to fully cover a requirement?

The answer to these questions typically relies on manual reviews.

Based on the Universal Pattern specification method, we provide a meaningful and mathematically sound definition of requirements coverage. This coverage is automatically evaluated and reported for a given set of test cases. In case of uncomplete coverage, you can even generate missing test cases fully automatically.

100% Automated

Formalized Requirements = Higher Quality

Thanks to the machine-readable nature of the formalized requirements, you can directly use them within several verification use cases and dramatically improve the quality and completeness of the verification process:

Formal Test

In a traditional requirements-based testing process, each test case is only evaluated against the requirement from which is was derived. But what if test case N°5 violates requirement N°10? Formal Test performs an automatic cross check of all test cases against all formalized requirements. This allows you to detect side effects without any additional testing effort.

Automatic Test Generation

Should a particular formal requirement not be fully covered by existing test cases, the Requirements-based Test Generation add-on allows generating missing test cases automatically, providing you 100% coverage for all requirements.

Formal Verification

Thanks to our powerful model checking technology, you can automatically obtain mathematically complete proof which guarantees a safety requirement can never be violated by your implementation. In case a requirement can be violated, we generate a counter example in the form of a test case.

认证

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的最高工具置信度。 我们根据要求免费向客户提供证书和相应的报告,这大大减少甚至消除了客户方工具认证措施的任何努力
ISO 26262 Certificate

申请试用License

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

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

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

申请试用license

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

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

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

BTC EMBEDDED SYSTEMS BLOG

From our Blog

Sharing insights on embedded software development, model-based design, automatic code generation and ISO 26262 compliant testing.

PRODUCT VIDEOS, VIDEO BLOG & WEBINARS

Videos & Webinars

Discover some of the main features of our products in these short videos.

BTC EmbeddedSpecifier

Step into the formal world with ease!