Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Actors for Timing Analysis of Distributed Redundant Controllers

  • 章节

  • 发表日期：

    2026年

查看全文
  • Marjan Sirjani,
  • Edward A. Lee,
  • Zahra Moezkarimi,
  • Bahman Pourvatan,
  • Bjarne Johansson,
  • Stefan Marksteiner,
  • Alessandro V. Papadopoulos

摘要

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.