diff --git a/subcommittee/tooling/mission-statement.md b/subcommittee/tooling/mission-statement.md index 57678697..11124900 100644 --- a/subcommittee/tooling/mission-statement.md +++ b/subcommittee/tooling/mission-statement.md @@ -6,11 +6,29 @@ ## State of Rust Safety-Critical Tooling -| Purpose | Requirement | Tool | Status | -|---------|-------------|------|--------| -| Qualified Compiler | ? | [Ferrocene](https://ferrocene.dev/en/) | Available for `aarch64-nostd` | -| Certified Core Library | SIL-4 / ASIL-D out of context | N/A | In progress by Ferrocene / Adacore / HighTec | -| Coding Style Verification | MISRA-C, ... | Rust Compiler, Clippy and probably additional tools required to verify and evaluate the application of the coding standard developed by the Code Guidelines Subcommittee | OxidOS can provide a mapping of MISRA-C Rules to the Rust Compiler | -| MC/DC Coverage report | ... | N/A | not available - LLVM might provide some tools | -| Static Analysis Tools | probably similar to Polyspace | N/A | an assesement about what the rust compiler covers is necessary | -| Code Metrics Generator | Cyclomatic Complexity, ... | N/A | not available | +| Need ID | Minimum Relevant Standard Rule | Tools | Notes | +|---------|--------------------------------|-------|-------| +| DC Coverage | ASIL-D, DAL-B | llvm (19, rustc 1.82) | - unstable, no macros / pattern matching | +| MC Coverage | ASIL-C. DAL-A | llvm (19, rustc 1.82) | - AdaCore report generator plans to stabilize the feature by end of 2025
- unstable, no macros / pattern matching | +| Statement Coverage | ASIL-A, DAL-C | llvm (19, rustc 1.82), [cargo-tarpaulin](https://github.com/xd009642/tarpaulin) | - unstable, no macros / pattern matching | +| 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 | +| 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 | +| Static Analysis Tools | DAL-C | | - make sure coding guidelines specify some rules, probably similar to Polyspace,
- an assessment about what the rust compiler covers is necessary
- 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
- [creusot](https://github.com/creusot-rs/creusot) WIP, works only for safe rust
- gillian-creusot WIP, not in a usable state, works for unsafe rust, [kani](https://model-checking.github.io/kani/) | - prove absence of UB
- prove that the code does what it should do
- using some spec (different language, eg SPARC or CodeProver, prove that an output is not possible) | +| Code Metrics - Cyclomatic Complexity | DAL-C | clippy - knows some sort of estimation as it complains if a function is too long. | - DO-178 linked to source code conformity - tightly linked the code guidelines
- Ada Core has a tool on the roadmap eventually | +| Code Traceability | DO-178 TBD | [mantra](https://crates.io/crates/mantra) - uses code annotation | | +| 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)
- cargo
- 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)
- 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) | + +## Standards Used + +- Automotive: ISO-26262 (ASIL) +- Aerospace: DO-178 (DAL)