Formal verification code of the ECU-switching MRM by tla+.
The code voter/ecu_switch.tla
verifies safety_island implementation mainly.
Formal verification code of the ECU-switching MRM by tla+.
The code voter/ecu_switch.tla
verifies safety_island implementation mainly.