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.
1. The model is completely synchronous...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.
Yes, it is the intended behavior. SMs and CMs are parameterized components, each of those having the same states and transitions wrt. its peers. See, "Automated Formal Verification of the TTEthernet Synchronization Quality" and note that we translated a SAL model to a SpaceEx model.
2. The CM1 and CM2 automata are *exactly* the same...Why do we need both of them?
As the paper above mentioned says: "for fault-tolerance reasons a TTEthernet network can implement redundant channels", hence there exists a second CM component which is also modeled in both, SAL and SpaceEx. Each CM uses a compression function which is the median of the
SM1_clock,...,SM5_clock values. Since SpaceEx does not offer a median function, and it is not practical to do that by hand even for small models, for simplicity we then assumed that the SM3_clock value is the median of those five values always.
3. Verification results with SpaceEx.
Fixed, see the updated files.
4. The properties specified for the models with 7 and 9 SMs seem wrong.
Fixed, see the updated files.
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.
Clocks in SM components belong to a different equivalence class of quasi-dependent variables wrt. those from CM components.
We arbitrarily incremented the number of SM components (the number of CM components is fixed), since we were playing with the scalability results, and comparing verification time before and after reducing quasi-dependent variables.
Best regards.
Hi Chtistian, thank you for taking the time to clarify my questions.
We can consider this version of the benchmark for the competition.
Sergio