Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark
Verification of Fault-Tolerant Clock Synchronization Algorithms Benchmark
The TTEthernet benchmark (http://cps-vo.org/node/26547) seems the only one with a picewise constant dynamic among the ARCH benchmark (please, tell me if there are others).
I tried to run the models (http://cps-vo.org/node/26534) with the provided configuration scripts with SpaceEx.
I have several doubts on the benchmark.
@Sergiy Bogomolov: since you are one of the authors of the models, could you please take a look at the following questions and provide some clarifications?
I was planning to use the model for different tasks (not just proving safety, but also synthesise parameters). I am currently stuck due to these issues.
1. The model is completely synchronous
All the automata (CM1, CM2, SM1, ...) synchronize on the same labels sync, send, and back.
This means that if CM1 moves on a transition labeled with sync, then all the other automata must also move on a transition labeled with sync (the same for send and back).
Now all the SMs and CMs move synchronously on send, sync and back, and there are never asynchronous actions.
Is it the intended behavior of the model?
From what I remember the TTEthernet model used in the papers by Wilfred Steiner have an asynchronous behavior.
2. The CM1 and CM2 automata are *exactly* the same.
The two CMs always read from the same SM, and never from different CMs. Their input parameters and labels are the same.
Why do we need both of them?
3. Verification results with SpaceEx
The verification, already for TTEthernet_Simplified_5.xml, terminates using the given configuration file TTEthernet_Simplified_5.cfg, but it does *NOT* reach a fix point.
Spaceex reaches the limit of 500 iterations and stops, but the property is not proved.
I increased the maximum number of iterations and left the model checker run for a while (1 hour), without seeing it terminate.
Is it the expected verification result? What are the results reported in the benchmarks description?
4. The properties specified for the models with 7 and 9 SMs seem wrong.
The properties for 7 and 9 SMs do not have the inequalities between all the possible pairs.
For example, in the one with 7 SMs the property for SM1_x - SM_6 > 2 * max_drift is missing (it seems an issue given by copying the property from the example with 5 SMs).
5. Adding more SM automata in the protocol does not seem very useful.
One just need two SMs, the one that is used by the CMs to read the clock value and another that tries to sync its clock.