AUTOSAR

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.