Your Solution for Safe Parallelization
The emmtrix Qualification Kit for emmtrix Parallel Studio (ePS-QKIT)* provides the tools and processes required for the safety qualification of emmtrix Parallel Studio according to DO-178C/330, ISO 26262 and comparable functional safety standards. This enables the use of our parallelization technology for safety-critical software of the highest safety levels. The QKIT is based on a verification tool that checks whether the sequential software (input) and the parallelized software (output) behave in exactly the same way.
* ePS-QKIT will be commercially available in Q4/2021
Our Qualification Strategy
The emmtrix Qualification Kit consists of our verification tool called the emmtrix Parallel Checker (ePC) that is running in the operational environment of the end user. The parallel checker may be run after each parallelization to prove the correctness of the parallel C code and generate relevant safety documents. It utilizes static code analysis to compare the sequential C and parallel C code. The check is only successful if the parallel code contains exactly the same calculations as the original code and is free of parallelization errors (such as race conditions, deadlocks, synchronization and communication faults).
This qualification strategy eliminates the risks (wrong behavior) of emmtrix Parallel Studio by checking the correctness of parallelization. The risk (fail to detect wrong behaviour) of the correctness check is lesser and is eliminated by qualification of the checker using the qualification kit. This enables the use of emmtrix Parallel Studio for parallelization of safety-critical software up to the highest safety levels.
- Performs a formal equivalence check with the help of an additional verification tool
- The verification tool runs after each parallelization
- Guarantees functional correctness
- Proves the absence of deadlocks and race conditions
- Detects potential errors introduced by ePS
- Generates safety reports
- Retains safety certification of input code
- Verification tool developed with different programming languages and technology for common cause avoidance
- Bidirectional traceability of statements between sequential and parallel C code
- Applicable up to the highest ISO 26262 safety levels (ASIL-D)
- Uses “validation of the software tool” qualification method
- Verification tool qualifiable according to TQL 5
- Verification tool can be used to eliminate and reduce verification processes on parallel code
- Applicable up to DAL-C projects
- TQL 4 and DAL-A on request
Our Verification Tool Report
The report of the verification tool provides a bidirectional traceability of the sequential input code (left) and the parallel output code (right). In this example, one function is split into two parallel functions, each running on a different core. The ePS has inserted communication statements (EMXAPI_Send and EMXAPI_Recv) into the parallel source code. The verification tool automatically finds matching statements on the right and left side and visualizes the matching in the report. Sensitive statements (which may affect the outcome of the program) are marked as red.
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 879405