- Software reliability is often defined by industry standards.
- Software analysis can be divided into three parts:
- Static analysis
- Examines code, no compilation or execution.
- Share input with compilers
- Example static analisers:
- BLAST, Cppcheck, Eclipse, Frama-C
- Splint - used by
- Proof systems
- Model checking
- Performs patter matching
- Understands c-types
- Language model and rule matching
- Control and data flow analysis
- Similar to compiler setup
- Run against entire application code.
- Improved auto generated code and readability.
- Found incorrect character conversion.
- Discovered signal sets unintentionally returning a boolean,
- Some false positives with unused code.
- Some macros were not picked up.
- Some variable initialisation not picked up.
- Works very well over all.
Felt the time invested in using splint was well spent and brings a lot of piece
of mind to the project.
- Uses CBMC
- Requires a little plumbing code and training.
- Made them reconsider and improve execution timing.
- Scalability requires improvements.
- Being integrated with eChronos.
Are we there yet?
- Static analysis Open Source tools need improving and an established best
- Model checking is not yet out of the box