[tooling] State of the safety critical tools #175
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
alexandruradovici
changed the title
MerrimanInd
reviewed
Feb 11, 2025
| | Function coverage | ASIL-C, DAL-C | llvm (19, rustc 1.82) - unstable, no macros / pattern matching, [cargo-tarpaulin](https://github.com/xd009642/tarpaulin) | | ||
| | Call coverage | ASIL-C, DAL-C | llvm (19, rustc 1.82), [cargo-tarpaulin](https://github.com/xd009642/tarpaulin) | - unstable, no macros / pattern matching | | ||
| | Branch Coverage | ASIL-B, DAL-C | llvm (19, rustc 1.82), [cargo-tarpaulin](https://github.com/xd009642/tarpaulin) | - unstable, no macros / pattern matching | | ||
| | Qualified Compiler | ASIL-D, DAL-D | ferroccene, Ada Core | |
There was a problem hiding this comment.
I believe the HighTec LLVM based compiler is also ASIL-D certified.
There was a problem hiding this comment.
ISO 26262 certified for Tricore
released, but not certified for arm
| | Qualified Compiler | ASIL-D, DAL-D | ferroccene, Ada Core | | ||
| | Fault Injection Tests | ASIL-D, DAL-D | N/A | | | ||
| | Test Coverage | ASIL-, DAL-D | llvm (19), cargo-test, [mantra?](https://crates.io/crates/mantra) | | | ||
| | Underfined Behaviour Absence | ASIL-A, DAL-C | ensured by static analysis and source code confirmity | |
There was a problem hiding this comment.
I think Miri calls itself an UB detection tool so maybe that should slot in here? Or elsewhere?
| | Underfined Behaviour Absence | ASIL-A, DAL-C | ensured by static analysis and source code confirmity | | ||
| | Static Analysis Tools | DAL-C | | - make sure coding guidelines specify some rules, probably similar to Polyspace, <br> - an assessment about what the rust compiler covers is necessary <br> - for DO-178 such tools support the *source code conformity* objective | | ||
| | Unambiguous Graphical Representation | ASIL-B | UML like too, but for Rust, AUTOSAR suggests - [Explanation of ARA Applications in Rust](https://www.autosar.org/fileadmin/standards/R23-11/AP/AUTOSAR_AP_EXP_ARARustApplications.pdf) | | ||
| | Formal Verification | ASIL-C (recommended), DAL-C (recommended) | - [verifast](https://github.com/verifast/verifast) WIP <br> - [creusot](https://github.com/creusot-rs/creusot) WIP, works only for safe rust <br> - gillian-creusot WIP, not in a usable state, works for unsafe rust, [kani](https://model-checking.github.io/kani/) | - prove absence of UB <br> - prove that the code does what it should do <br> - using some spec (different language, eg SPARC or CodeProver, prove that an output is not possible) | |
There was a problem hiding this comment.
Verus is in beta but a formal verification tool that might get thrown in here.
| | Use of naming convention | ASIL-A | Clippy | Not available tool that allow to define and enforce naming convention. Clippy check only for predefined and generic naming convention | | ||
| | Measurement of execution time and reaction time of software unit | ASIL-A (depends in the requirements) | perf, Intel VTune, flamegraph, [Rapita](https://www.adacore.com/press/rapita-systems-showcases-adacores-gnat-pro-for-rust-at-hisc) | For hard realtime application are required not intrusive profiler that are typically HW specific | | ||
| | Test runner | all | - [cargo-nextest](https://nexte.st) <br> - cargo <br> - defmt-test + probe.rs | No ISO qualified tool are available. Example of qualified test runner: [VectorCast](https://www.vector.com/us/en/products/products-a-z/software/vectorcast/?gad_source=1&gclid=EAIaIQobChMIyMKCgvn3igMVM0-RBR1s9BOkEAAYASAAEgJM2_D_BwE#c336977), [TESSY](https://www.razorcat.com/en/product-tessy.html) <br> - tightly linked to the coverage level | | ||
| | Automatic generation of unit/integration tests based on equivalence classes and boundary values | ASIL-B | | Example of automatic test generator based on equivalence classe and boundary values: [VectorCast](https://www.vector.com/us/en/products/products-a-z/software/vectorcast/?gad_source=1&gclid=EAIaIQobChMIyMKCgvn3igMVM0-RBR1s9BOkEAAYASAAEgJM2_D_BwE#c336977), [TESSY](https://www.razorcat.com/en/product-tessy.html) | |
There was a problem hiding this comment.
Would property based testing like proptest fit in here?
|
Was notified of I know we had the discussion last time that the Venn diagram of "safety-critical standards" and "formal methods" tend to have little to no overlap, but thought I'd mention it as it came up here. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request adds a list of requirements and existing tools of safety critical certification. This reflects the results of the meetings of the tooling subcommittee.
@af-airbus please take a look at the DAL related entries, some of the lines in the table do not have a DAL minimum requirements
@jgust @Bgenis @pellico and @jmqd please take a look at the ASIL minimum ASIL items, some of the lines of the table arte missing ASIL