Specification and verification of a multi-agent coordination protocol with TLA+
Resumo
There is a general rule which says that about 50 percent of the elapsed time in a project is expended in testing. Finding bugs in software might be an awkward task, especially when there are design errors. The common sense, however, frequently has a biased view of formal methods, associating it with high complexity and low return on investment. That would supposedly be worth only for critical parts of a system. TLA + is a formal specification language that is based on first-order logic and set theory. In this paper, we describe how we used it to formally specify a coordination protocol and how we applied model checking technique to verify correctness properties. We also discuss the advantages of TLA + and the relatively low overhead to get used to it.
Palavras-chave:
TLA , Industrial Control Systems, Formal Methods, Model Checking, Coordination, Security
Referências
J. M. Wing, “Program specification,” in Encyclopedia of Computer Science. Chichester, UK: John Wiley and Sons Ltd., pp. 1454–1458.
L. Lamport, J. Matthews, M. Tuttle, and Y. Yu, “Specifying and Verifying Systems with TLA+,” in Proceedings of the 10th Workshop on ACM SIGOPS European Workshop, ser. EW 10. New York, NY, USA: ACM, 2002, pp. 45–48.
C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon Web Services Uses Formal Methods,” Commun. ACM, vol. 58, no. 4, pp. 66–73, Mar. 2015.
C. Newcombe, “Why Amazon Chose TLA+,” in Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477, ser. ABZ 2014. New York, NY, USA: Springer-Verlag New York, Inc., 2014, pp. 25–39.
B. Batson and L. Lamport, “High-level specifications: Lessons from industry,” in Formal Methods for Components and Objects. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 242–261.
D. Shukla, “A technical overview of azure cosmos db,” https://azure.microsoft.com/en-us/blog/a-technical-overview-of-azure- cosmos-db/, May 2017, [Online; accessed 16-April-2018].
L. Lamport, “Byzantizing paxos by refinement,” Distributed Computing: 25th International Symposium, pp. 211–224, June 2011. [Online]. Available: https://www.microsoft.com/en- us/research/publication/byzantizing-paxos-refinement/
T. Lu, S. Merz, and C. Weidenbach, “Towards Verification of the Pastry Protocol Using TLA+,” in Proceedings of the Joint 13th IFIP WG 6.1 and 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, ser. FMOODS’11/FORTE’11. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 244–258.
D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “Tla+ proofs,” Proceedings of the 18th International Symposium on Formal Methods (FM 2012), vol. 7436, pp. 147–154, January 2012.
J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, “Formal specification of a Web services protocol,” The Journal of Logic and Algebraic Programming, vol. 70, no. 1, pp. 34–52, 2007.
R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. Tuttle, and Y. Yu, “Checking Cache-Coherence Protocols with TLA+,” Formal Methods in System Design, vol. 22, no. 2, pp. 125–131, Mar 2003.
L. Lamport,“How to write a 21st century proof,”Journal of Fixed Point Theory and Applications, vol. 11, no. 1, pp. 43–63, Mar 2012.
D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “Tla+ proofs,” in 18th Intl. Symp. Formal Methods (FM 2012), ser. LNCS, D. Giannakopoulou and D. Me ́ry, Eds., vol. 7436. Paris, France: Springer, 2012, pp. 147–154.
C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, “Ironfleet: Proving practical distributed systems correct,” in Proceedings of the 25th Symposium on Operating Systems Principles, ser. SOSP ’15. New York, NY, USA: ACM, 2015, pp. 1–17.
L. Lamport, “The temporal logic of actions,” ACM Trans. Program. Lang. Syst., vol. 16, no. 3, pp. 872–923, May 1994.
——,“The TLA Home Page,”https://lamport.azurewebsites.net/tla/tla.html, [Online; accessed 21-April-2018].
——, “What Good is Temporal Logic?” Information Processing,vol.83, pp. 657–668, 1983.
B. Alpern and F. B. Schneider, “Defining liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181–185, 1984.
L. Lamport, “Proving the correctness of multiprocess programs,” IEEE Transactions on Software Engineering, vol. 3, no. 2, pp. 125–143, Mar. 1977.
S. Merz, The Specification Language TLA+. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 401–451.
L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston,MA,USA:Addison-Wesley Longman Publishing Co., Inc., 2002.
“SCISSOR - Security in Trusted SCADA and Smart-Grids,” https://scissor-project.com/, [Online; accessed 26-May-2018].
B. Zhu, A. Joseph, and S. Sastry, “A taxonomy of cyber attacks on SCADA systems,” in Proceedings of the 2011 International Conference on Internet of Things and 4th International Conference on Cyber, Physical and Social Computing, ser. ITHINGSCPSCOM ’11. Washington, DC, USA: IEEE Computer Society, 2011, pp. 380–388.
K. Stouffer, J. Falco, and K. Kent, “Guide to Supervisory Control and Data Acquisition (SCADA) and Industrial Control Systems Security,” January 2006.
C. Brandauer, P. Dorfinger, and P. Y. A. Paiva, “Towards scalable and adaptable security monitoring,” in 2017 IEEE 36th International Performance Computing and Communications Conference (IPCCC), Dec 2017, pp. 1–6.
P. Y. A. Paiva, O. Saotome, and C. Brandauer, “Demonstrating the feasibility of a new security monitoring framework for SCADA systems,” in 2017 3rd Brazilian Technology Symposium (BTSym’17), Dec 2017, pp. 1–6.
M. Abadi and L. Lamport, “The existence of refinement mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253–284, May 1991.
L. Lamport and S. Merz, “Auxiliary Variables in TLA+,” Inria Nancy - Grand Est (Villers-le`s-Nancy, France) ; Microsoft Research, Research Report, Mar. 2017. [Online]. Available: https://hal.inria.fr/hal-01488617
L. Lamport, J. Matthews, M. Tuttle, and Y. Yu, “Specifying and Verifying Systems with TLA+,” in Proceedings of the 10th Workshop on ACM SIGOPS European Workshop, ser. EW 10. New York, NY, USA: ACM, 2002, pp. 45–48.
C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, “How Amazon Web Services Uses Formal Methods,” Commun. ACM, vol. 58, no. 4, pp. 66–73, Mar. 2015.
C. Newcombe, “Why Amazon Chose TLA+,” in Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477, ser. ABZ 2014. New York, NY, USA: Springer-Verlag New York, Inc., 2014, pp. 25–39.
B. Batson and L. Lamport, “High-level specifications: Lessons from industry,” in Formal Methods for Components and Objects. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 242–261.
D. Shukla, “A technical overview of azure cosmos db,” https://azure.microsoft.com/en-us/blog/a-technical-overview-of-azure- cosmos-db/, May 2017, [Online; accessed 16-April-2018].
L. Lamport, “Byzantizing paxos by refinement,” Distributed Computing: 25th International Symposium, pp. 211–224, June 2011. [Online]. Available: https://www.microsoft.com/en- us/research/publication/byzantizing-paxos-refinement/
T. Lu, S. Merz, and C. Weidenbach, “Towards Verification of the Pastry Protocol Using TLA+,” in Proceedings of the Joint 13th IFIP WG 6.1 and 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, ser. FMOODS’11/FORTE’11. Berlin, Heidelberg: Springer-Verlag, 2011, pp. 244–258.
D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “Tla+ proofs,” Proceedings of the 18th International Symposium on Formal Methods (FM 2012), vol. 7436, pp. 147–154, January 2012.
J. E. Johnson, D. E. Langworthy, L. Lamport, and F. H. Vogt, “Formal specification of a Web services protocol,” The Journal of Logic and Algebraic Programming, vol. 70, no. 1, pp. 34–52, 2007.
R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. Tuttle, and Y. Yu, “Checking Cache-Coherence Protocols with TLA+,” Formal Methods in System Design, vol. 22, no. 2, pp. 125–131, Mar 2003.
L. Lamport,“How to write a 21st century proof,”Journal of Fixed Point Theory and Applications, vol. 11, no. 1, pp. 43–63, Mar 2012.
D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “Tla+ proofs,” in 18th Intl. Symp. Formal Methods (FM 2012), ser. LNCS, D. Giannakopoulou and D. Me ́ry, Eds., vol. 7436. Paris, France: Springer, 2012, pp. 147–154.
C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill, “Ironfleet: Proving practical distributed systems correct,” in Proceedings of the 25th Symposium on Operating Systems Principles, ser. SOSP ’15. New York, NY, USA: ACM, 2015, pp. 1–17.
L. Lamport, “The temporal logic of actions,” ACM Trans. Program. Lang. Syst., vol. 16, no. 3, pp. 872–923, May 1994.
——,“The TLA Home Page,”https://lamport.azurewebsites.net/tla/tla.html, [Online; accessed 21-April-2018].
——, “What Good is Temporal Logic?” Information Processing,vol.83, pp. 657–668, 1983.
B. Alpern and F. B. Schneider, “Defining liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181–185, 1984.
L. Lamport, “Proving the correctness of multiprocess programs,” IEEE Transactions on Software Engineering, vol. 3, no. 2, pp. 125–143, Mar. 1977.
S. Merz, The Specification Language TLA+. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 401–451.
L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston,MA,USA:Addison-Wesley Longman Publishing Co., Inc., 2002.
“SCISSOR - Security in Trusted SCADA and Smart-Grids,” https://scissor-project.com/, [Online; accessed 26-May-2018].
B. Zhu, A. Joseph, and S. Sastry, “A taxonomy of cyber attacks on SCADA systems,” in Proceedings of the 2011 International Conference on Internet of Things and 4th International Conference on Cyber, Physical and Social Computing, ser. ITHINGSCPSCOM ’11. Washington, DC, USA: IEEE Computer Society, 2011, pp. 380–388.
K. Stouffer, J. Falco, and K. Kent, “Guide to Supervisory Control and Data Acquisition (SCADA) and Industrial Control Systems Security,” January 2006.
C. Brandauer, P. Dorfinger, and P. Y. A. Paiva, “Towards scalable and adaptable security monitoring,” in 2017 IEEE 36th International Performance Computing and Communications Conference (IPCCC), Dec 2017, pp. 1–6.
P. Y. A. Paiva, O. Saotome, and C. Brandauer, “Demonstrating the feasibility of a new security monitoring framework for SCADA systems,” in 2017 3rd Brazilian Technology Symposium (BTSym’17), Dec 2017, pp. 1–6.
M. Abadi and L. Lamport, “The existence of refinement mappings,” Theoretical Computer Science, vol. 82, no. 2, pp. 253–284, May 1991.
L. Lamport and S. Merz, “Auxiliary Variables in TLA+,” Inria Nancy - Grand Est (Villers-le`s-Nancy, France) ; Microsoft Research, Research Report, Mar. 2017. [Online]. Available: https://hal.inria.fr/hal-01488617
Publicado
06/11/2018
Como Citar
PAIVA, Pedro Yuri Arbs ; SAOTOME, Osamu; BRANDAUER, Christof.
Specification and verification of a multi-agent coordination protocol with TLA+. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SISTEMAS COMPUTACIONAIS (SBESC), 8. , 2018, Salvador.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2018
.
p. 155-160.
ISSN 2237-5430.
