Usable formal methods - are we there yet? - Stefan Götz - LCa2016

Stefan Götz

• 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
      • LLVM/CLang
      • Sparse
      • Splint - used by eChronos
  • Proof systems
  • Model checking

Splint

• 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.

Model Checking

• 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 practices.
• Model checking is not yet out of the box