Play now
Play Video
Play now
Play Video
Close
Intuitive formal specification of safety 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.
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:
In the first step, individual expressions or events within the requirement are identified as so-called “macros.”
In a second step, these macros get graphically structured to define their relationship and timing behavior.
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.
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.
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:
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.
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.
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.
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 IEC 61508-3:3010, ISO 26262, EN 50128, IEC 62304 as well as ISO 25119.
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.
If you would like to try out our tools, we will gladly provide an evaluation license free of charge. Evaluations include a free launch workshop and also provide an opportunity for you to meet one-on-one with our support and engineering teams.
Do you have any questions or want to see our tools in action? If so, please use the link below to schedule a meeting, where a member of our engineering team will be happy to show you the features and use cases and directly answer any questions you might have.
If you would like to try out our tools, we will gladly provide an evaluation license free of charge. Evaluations include a free launch workshop and also provide an opportunity for you to meet one-on-one with our support and engineering teams.
Do you have any questions or want to see our tools in action? If so, please use the link below to schedule a meeting, where a member of our engineering team will be happy to show you the features and use cases and directly answer any questions you might have.
Step into the formal world with ease!
We provide intelligent and automated test solutions which enable our customers to deal with the growing complexity of embedded software while achieving high quality in compliance with the ISO 26262 standard.
Copyright © 2024 BTC Embedded Systems
