This page gives supplemental information about the submitted paper that studies timeout order abstraction. I am currently updating this page and adding more information, so please visit the page again soon to see more information.

We need some more time to revise wording in the draft of a technical report version of the submitted appear. Therefore, we put supplemental technical contents for the submitted paper as appendices. The above appendices include the entire template set, a formal definition of the abstraction, and the soundness proof. ** The appendices are updated on Nov. 20th. We newly included a section for the DHCP-F case study, and revised the simulation-relation definition in the soundness section.

We have uploaded a draft (a stable version) of the technical report that describes TO-Abstraction.

We have put three pieces of SAL code. The first one is for the resource-sharing protocol, and the remaining two are for the DHCP-F protocol. All pieces of code represent untimed models obtained from TO-abstraction.

This SAL code is for the resouce-sharing protocol. It represents the untimed model of our implementation of the time-sharing protocol that we describe in the submitted paper (the complete Tempo code will appear in the technical report version). This untimed model is obtained from TO-abstraction. (We applied abstraction manually for this case study). The code currently use the configuration of [#RED = 2, #BLUE = 2], where RED and BLUE represents the two groups of processes for resource-sharing. Using this configurration, we verified the protocol up to depth 20 using the SAL bounded model-checker.

This SAL code is for the DHCP-F protocol. It represents the untimed model of the DHCP-F protocol (the complete Tempo code will appear in the technical report version). This untimed model is obtained from TO-abstraction. (We applied abstraction manually for this case study). The code currently use the configuration of [#Servers = 2, #Clients = 2]. Using this configurration, we verified the protocol up to depth 20 using the SAL bounded model-checker.

This SAL code is a mutated version of the DHCP-F model described above. In this version, the server updates its estimate of backup server's timeouts without checking the interaction instance of the received message from a backup server. We conducted bounded model-checking for this mutated version, and found a counterexample at depth 17. We will show a detailed analysis of this counterexample in the technical report version of the paper. The actual counterexample trace can be found here. We produced this HTML file by converting the counterexample report from SAL, which was in the raw text format.