SAL files for "A Formally Verified Reintegration Protocol"

Email the author, Lee Pike, at lee.s.pike@nasa.gov with any questions or inquiries.

EMSOFT 2005 Paper Download emsoft.pdf
Technical Paper Download: reint.pdf
Synchronizing Timeout Automata Model of the Train-Gate-Controller in SAL (Appendix A): sta_tgc.sal
Synchronizing Timeout Automata Model of the Train-Gate-Controller in SAL with clockless semantics (Appendix B): sta_tgc_clockless.sal
Reintegration Protocol Model in SAL: reint.sal
Proof Script Download: prf.sh
(The model of the reintegration protocol contains multiple propositions, so a script to rerun the k-induction proofs for this model has been provided. The script is borrowed from Bruno Dutertre's script for the SAL proofs he completed for the paper Modeling and Verification of a Fault-Tolerant Real-Time Startup Protocol using Calendar Automata authored by Dutertre and M. Sorea.)