In the automotive sector, AUTOSAR establishes standards for architecture, communication and deployment for software and sensor/actuator functionality. A model-driven development approach enables the generation of many of the required artifacts encoded as ARXML.
Here is a PhD thesis describing formal verification of such a system.

Related Articles
Dear Modelers, Significant progress has been made on a specifications of textual xtUML and separately…
At xtUML Days 2020 UK, Marc Balcer explained model-driven test case generation with TAME.
BridgePoint is Open Source Software (OSS). It is free. However, OSS is not free like…