Static Analysis Tools
Verification of Software and in particular Software for Embedded Systems is a challenging task that involves approaches from various domains ranging from rigid code reviews, over exhaustive tests up to formal methods.
In the context of this workpackage we are evaluating, adapting, and developing various tools in the fields of static analysis and model checking focusing on Embedded Software. In particular, we evaluate open-source static analysis tools for C code like cppcheck, Splint, or Frama-C on code written for Cortex-M microcntrollers as used in various classes on Embedded Systems Software Design at the University of Applied Sciences Technikum Wien. Furthermore, we intend to adapt an approach as used by Frama-C in combination with the ANSI/ISO C Specification language to enrich code with contracts and verify the latter against the implementation.
In the field of model checking, we pursue the goal to evaluate several existing model-checkers like CBMC or UPPAAL for their applicability in our classes in order to improve design and verification aspects of the projects implemented in class or along various bachelor or master projects.
