BTC EmbeddedSpecifier

Step into the formal world with ease!

What if your PC could understand your requirements?

Step into the formal world with ease

BTC EmbeddedSpecifier is a tool used to create and manage semi-formal and formal requirements for safety-critical projects. While a semi-formal and formal notation of requirements is recommended in standards like ISO 26262 and IEC 61508, most formal notation languages require a high level of expert knowledge to both read and write them. Instead of having to create formal requirements from scratch, BTC EmbeddedSpecifier provides you with an intuitive method to derive comprehensible formal requirements from natural language without expert knowledge.

Formalized requirements = Better requirements

In most development projects today, requirements are created and managed using informal natural language in tools such as IBM DOORS or PTC Integrity. 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, requirements can be transformed 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.In most development projects today, requirements are created and managed using informal natural language in tools such as IBM DOORS or PTC Integrity. 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, requirements can be transformed 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.

Universal Pattern - Welcome to the formal world

From our perspective, there are two primary reasons formal notations have not gained more acceptance in embedded development projects until now. Formal languages like LTL are often considered to be too difficult to use and they do not provide enough traceability towards existing informal requirements. With Universal Pattern, both issues are efficiently addressed. A typical formalization workflow starts with the import of existing natural language requirements. In the first step, individual expressions or events within the requirement have to be identified as so-called macros. In a second step, these macros need to be structured to define their relationship and timing behavior – delivering a semi-formal representation as an intermediate result. You will start with a very simple structure and then refine it where needed – keeping the formal requirement as simple as possible while remaining as complex as needed. A graphical representation of the Universal Pattern serves as an editor and at the same time as documentation, making the formal requirement easy to understand and review. 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.

A meaningful definition of requirement coverage

With natural language requirements, definition of requirement coverage is always a tricky question. As long as a requirement is not machine-readable, the decision if it has been covered and if the coverage is complete is typically based on a manual review of the related test cases.

Based on the Universal Pattern specification method, a new definition of requirement coverage has been identified and mathematically defined in order to allow the measurement of requirement coverage in a completely automated way.

Formalized requirements = Better verification

Thanks to the machine-readable nature of the formalized requirements, they can be introduced in several verification use cases and dramatically improve the quality and completeness of the verification process. Examples are:

Formal Test with BTC EmbeddedTester BASE
Requirements-based Test Generation with BTC EmbeddedTester BASE
Formal Verification with BTC EmbeddedValidator

BTC EmbeddedSpecifier even provides two add-ons which allow exporting the formalized requirements into so called “Requirement Observers.” These can then be integrated into other test environments. Observers can either be exported as C-Code or in the dSPACE RTT format allowing them to run in real-time on a dSPACE platform.