Proceedings of the NASA Formal Methods Symposium, pp. 255–262
2019 · doi: 10.1007/978-3-030-20652-9_17
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.
subject terms: Model-based Systems Engineering, MbSE