This page explains how you can reproduce the timing parameter synthesis results for the biphase mark protocol (BMP).

The first step is model-checking the discretized model of BMP by using the SAL symbolic model-checker. You can download the following SAL code, and then check the theorems using the sal-smc command.
[SAL code for a discretized biphase mark protocol model].

The next step is deriving parameter constraints using METEORS. To do so, you have to first download the METEORS module implemented in Python.
[METEORS module file (compiled Python code)].
Then, you have to download the following code in the same directory as the METEORS module is located in, and run the code in Python.
[Python file that uses METEORS to derive parameter constraints for the biphase mark protocol].
If you are successful (which I hope you should be), then you will see that the three constraints explained in the paper are automatically derived from the specified event orders. METEORS also lists sufficient constraints for each of the specified event orders. You can also try adding event orders one by one to METEORS and see the results. You can find the instruction to do this in the above Python file.