EVA is a framework for the integration of modern verification tools in the context of AUTOSAR, a widely-used open stan- dard for the development of automotive software systems. EVA enables the automatic end-to-end verification of system-level properties using a compositional approach. It combines software model checking techniques for the verification of software components at the code level with a contract-based analysis for verifying their correct composition.

A description of the tool has been published by Springer as part of the proceedings of TACAS 2023 (Springer link).

• Material:
  • Preprint version of the paper
  • Kratos verification benchmarks used in the case study
  • OCRA verification benchmarks used in the case study