Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking

Alastair Donaldson's PhD thesis obtained from the Department of Computing Science, University of Glasgow, under the supervision of Alice Miller

Code Examples from Thesis

All specifications are in Promela, unless otherwise specified

For each specification, the associated section and/or appendix in the dissertation is also provided. All specifications are given in .txt format

• Simple mutual exclusion (Sections 2.4.1 and 4.2.1)
• Simple mutual exclusion - SymmSpin version (Sections 3.3.2 and 4.2.1)
• Simple mutual exclusion in SMC (Sections 3.3.3 and 4.2.2)
• Simple mutual exclusion with generic representatives (Section 3.5.2)
• Peterson's mutual exclusion protocol - SymmSpin version (Section 4.3.1, Appendix A.1.1)
• SymmSpin system description file for Peterson's mutual exclusion protocol (Section 4.3.1, Appendix A.1.1)
• Peterson's mutual exclusion protocol - simpler version (Section 4.3.2, Appendix A.1.2)
• Peterson's mutual exclusion protocol in SMC (Section 4.3.3, Appendix A.1.3)
• Peterson's mutual exclusion protocol - version with less atomicity (Section 4.3.4, Appendix A.1.4)
• Resource allocator (Section 4.4, Appendix A.2.1)
• Resource allocator in SMC (Section 4.4.2, Appendix A.2.2)
• Resource allocator with sharing (Section 4.4.3, Appendix A.2.3)
• Three-tiered architecture (Section 4.5, Appendix A.3)
• Message routing in a hypercube (Section 4.6, Appendix A.4.1)
• Loadbalancer in Promela-Lite (Section 6.5)
• Message routing in a hypercube, re-modelled without arithmetic (Section 8.4.1, Appendix A.4.2)
• Telephone specification - original (Section 8.5.4, Appendix A.5.1)
• Telephone specification - re-modelled (Section 8.5.4, Appendix A.5.2)
• Railway signalling system - original (Section 8.5.4, Appendix A.6.1)
• Railway signalling system - re-modelled (Section 8.5.4, Appendix A.6.2)