https://www.mdu.se/

We use two actor-based languages, Timed Rebeca and Lingua Franca, to show modeling, model checking, implementation, and timing analysis of an industry-suggested algorithm for role selection in distributed control systems with redundancy. The algorithm prioritizes consistency over availability in trade-off situations. We show scenarios that simulate the environment and possible faults and use the Timed Rebeca model checking tool to investigate whether they may cause a failure. We also show the maximum latency that can be tolerated without causing inconsistency. We then use the coordination language Lingua Franca to implement the model. It can also simulate network switches, allowing you to set up test scenarios that include network degradation, such as switch failures, packet losses, and excessive latency. This can be set up as a hardware-in-the-loop simulation, where the actual node implementations interact with simulated switches and the network.