Design and Runtime Verification Side-by-Side in eTrice

Sudeep Kanav, Levi Lúcio, Christian Hilden and Thomas Schuetz

Proceedings of the NASA Formal Methods Symposium, pp. 255–262

2019 · doi:10.1007/978-3-030-20652-9_17

abstract

eTrice is a mature open-source model-based software engineering tool, based on the ROOM methodology. It is currently used in the industry for the development of solutions for domains such as health, heavy machinery and the automotive. eTrice natively incorporates mechanisms for runtime verification. At the request of the developers of eTrice, we have incorporated model checking in their tool chain, by partly reusing the existing runtime verification architecture. We report on the implementation of the tool, experiments that we conducted, and lessons learned regarding the synergies between the two verification techniques.