Formal verification of mobile robot protocols. (English) Zbl 1410.68217
Summary: Mobile robot networks emerged in the past few years as a promising distributed computing model. Existing work in the literature typically ensures the correctness of mobile robot protocols via ad hoc handwritten proofs, which, in the case of asynchronous execution models, are both cumbersome and error-prone. Our contribution is twofold. We first propose a formal model to describe mobile robot protocols operating in a discrete space i.e., with a finite set of possible robot positions, under synchrony and asynchrony assumptions. We translate this formal model into the DVE language, which is the input format of the model-checkers DiVinE and ITS tools, and formally prove the equivalence of the two models. We then verify several instances of two existing protocols for variants of the ring exploration in an asynchronous setting: exploration with stop and perpetual exclusive exploration. For the first protocol we refine the correctness bounds and for the second one, we exhibit a counter-example. This protocol is then modified and we establish the correctness of the new version with an inductive proof.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68M12 | Network protocols |
| 68M14 | Distributed systems |
References:
| [1] | Flocchini, P., Prencipe, G., Santoro, N.: Distributed Computing by Oblivious Mobile Robots. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael, California (2012) · Zbl 1286.68484 |
| [2] | Almeida, A., Ramalho, G., Santana, H., Azevedo Tedesco, P., Menezes, T., Corruble, V., Chevaleyre, Y.: Recent advances on multi-agent patrolling. In: 17th Brazilian Symposium on Artificial Intelligence Advances in Artificial Intelligence—SBIA 2004, São Luis, Maranhão, Brazil, 29 Sept-1 Oct 2004, Proceedings, pp. 474-483 (2004) |
| [3] | Flocchini, P., Ilcinkas, D., Pelc, A., Santoro, N.: Computing without communicating: ring exploration by asynchronous oblivious robots. Algorithmica 65(3), 562-583 (2013) · Zbl 1272.68399 · doi:10.1007/s00453-011-9611-5 |
| [4] | Blin, L., Milani, A., Potop-Butucaru, M., Tixeuil, S.: Exclusive perpetual ring exploration without chirality. In: Proceedings of 24th International Symposium in Distributed Computing (DISC’10), vol. 6343 of LNCS, pp. 312-327. Springer (2010) · Zbl 1290.68114 |
| [5] | Suzuki, I., Yamashita, M.: Distributed anonymous mobile robots: formation of geometric patterns. SIAM J. Comput. 28(4), 1347-1363 (1999) · Zbl 0940.68145 · doi:10.1137/S009753979628292X |
| [6] | Clerentin, A., Delafosse, M., Delahoche, L., Marhic, B., Jolly-Desodt, A.: Uncertainty and imprecision modeling for the mobile robot localization problem. Auton. Robots 24(3), 267-283 (2008) · doi:10.1007/s10514-007-9066-3 |
| [7] | D’Angelo, G., Di Stefano, G., Navarra, A.: Gathering of six robots on anonymous symmetric rings. In: Proceedings of 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO’11), volume 6796 of LNCS, pp. 174-185. Springer (2011) · Zbl 1298.68270 |
| [8] | Kamei, S., Lamani, A., Ooshita, F., Tixeuil, S.: Asynchronous mobile robot gathering from symmetric configurations without global multiplicity detection. In: Proceedings of 18th International Colloquium on Structural Information and Communication Complexity (SIROCCO’11), vol. 6796 of LNCS, pp. 150-161. Springer (2011) · Zbl 1267.68143 |
| [9] | Lamani, A., Kamei, S., Ooshita, F., Tixeuil, S.: Gathering an even number of robots in an odd ring without global multiplicity detection. In: Proceedings of International Conference on Mathematical Foundations of Computer Science (MFCS’12), vol. 7464 of LNCS, pp. 542-553. Springer (2012) · Zbl 1365.68421 |
| [10] | Flocchini, P., Prencipe, G., Santoro, N., Widmayer, P.: Gathering of asynchronous robots with limited visibility. Theor. Comput. Sci. 337(1-3), 147-168 (2005) · Zbl 1108.68120 · doi:10.1016/j.tcs.2005.01.001 |
| [11] | Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001) · Zbl 0847.68063 · doi:10.1016/B978-044450813-3/50026-6 |
| [12] | Baier, C., Katoen, J .P.: Principles of Model Checking. MIT Press, Cambridge (2008) · Zbl 1179.68076 |
| [13] | Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Proceedings of Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’94), organized jointly with the Working Group Provably Correct Systems—ProCoS, vol. 863 of LNCS, pp. 41-76. Springer (1994) · Zbl 0940.68145 |
| [14] | Kulkarni, S.S., Bonakdarpour, B., Ebnenasir, A.: Mechanical verification of automatic synthesis of fault-tolerant programs. In: Proceedings of 14th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR’ 04), vol. 3573 of LNCS, pp. 36-52. Springer (2004) · Zbl 1134.68348 |
| [15] | Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput. 22(3), 129-145 (2010) · Zbl 1267.68143 · doi:10.1007/s00446-009-0092-6 |
| [16] | Chatzigiannakis, I., Michail, O., Spirakis, P.G.: Algorithmic verification of population protocols. In: Proceedings of 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’10), vol. 6366 of LNCS, pp. 221-235. Springer (2010) |
| [17] | Clément, J., Delporte-Gallet, C., Fauconnier, H., Sighireanu, M.: Guidelines for the verification of population protocols. In: Proceedings of 31st International Conference on Distributed Computing Systems (ICDCS’11), pp. 215-224. IEEE (2011) |
| [18] | Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: Proceedings of 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’11), vol. 6976 of LNCS, pp. 120-134. Springer (2011) |
| [19] | Lu, T., Merz, S., Weidenbach, C.: Towards verification of the pastry protocol using TLA \[^{{+}}+. In\]: Proceedings of Joint 13t International Conference (FMOODS’11) 2011, and 31st International Conference (FORTE’11) on Formal Techniques for Distributed Systems, volume 6722 of LNCS, pp. 244-258. Springer (2011) |
| [20] | Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distrib. Comput. 23, 341-358 (2011) · Zbl 1231.68164 · doi:10.1007/s00446-010-0123-3 |
| [21] | Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2 |
| [22] | Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual Symposium on Logic in Computer Science, pp. 352-359. IEEE (1999) |
| [23] | Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213-214 (1988) · Zbl 0664.68048 · doi:10.1016/0020-0190(88)90211-6 |
| [24] | Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Paolo, B., Daniele, G. (eds.) CONCUR 2014 Concurrency Theory, vol. 8704 of Lecture Notes in Computer Science, pp. 109-124. Springer, Berlin (2014) · Zbl 1417.68112 |
| [25] | Allen Emerson, E., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’95, pp. 85-94. ACM, New York (1995) · Zbl 1101.68371 |
| [26] | Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Proceedings of International Conference on Theoretical Aspects of Computer Software (TACS’94), vol. 789 of LNCS, pp. 726-765. Springer (1994) · Zbl 0942.03527 |
| [27] | Clarke, E.M., Grumberg, O., Jha, S.: Veryfying parameterized networks using abstraction and regular languages. In: Proceedings of 6th International Conference on Concurrency Theory (CONCUR’95), vol. 962 of LNCS, pp. 395-407. Springer (1995) |
| [28] | Bjørner, N., Browne, A., Chang, E.Y., Colón, M., Kapur, A., Manna, Z., Sipma, H., Uribe, T.E.: Step: deductive-algorithmic verification of reactive and real-time systems. In: Proceedings of 8th International Conference on Computer Aided Verification (CAV’96), vol. 1102 of LNCS, pp. 415-418. Springer (1996) |
| [29] | de Alfaro, L., Manna, Z., Sipma, H.B., Uribe, T.E.: Visual verification of reactive systems. In: Proceedings of 3rd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS’97), vol. 1217 of LNCS, pp. 334-350. Springer (1997) · Zbl 1002.68029 |
| [30] | Cansell, D., Méry, D., Merz, S.: Diagram refinements for the design of reactive systems. J. Univ. Comput. Sci. 7(2), 159-174 (2001) · Zbl 0970.68103 |
| [31] | Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Proceedings of 13th International Conference on Computer Aided Verification (CAV’01), vol. 2102 of LNCS, pp. 221-234. Springer (2001) · Zbl 0991.68541 |
| [32] | Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In Marco, B., Ferruccio, D., Reiner, H., EinarBroch, J., Ina S. (eds.) Formal Methods for Executable Software Models, vol. 8483 of Lecture Notes in Computer Science, pp. 122-171. Springer International Publishing (2014) · Zbl 1445.68133 |
| [33] | Devismes, S., Lamani, A., Petit, F., Raymond, P., Tixeuil, S.: Optimal grid exploration by asynchronous oblivious robots. In: Proceedings of 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’12), vol. 7596 of LNCS, pp. 64-76. Springer (2012) |
| [34] | Bonnet, F., Défago, X., Petit, F., Potop-Butucaru, M., Tixeuil, S.: Brief announcement: discovering and assessing fine-grained metrics in robot networks protocols. In: Proceedings of 14th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’12), vol. 7596 of LNCS, pp. 282-284. Springer (2012) |
| [35] | Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proc. IEEE 79(9), 1305-1320 (1991) · doi:10.1109/5.97300 |
| [36] | Barnat, J., Brim, L., Havel, V., Havlícek, J., Kriho, J., Lenco, M., Rockai, P., Still, V., Weiser, J.: Divine 3.0—an explicit-state model checker for multithreaded \[C \& C++\]++ programs. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV’13), vol. 8044 of LNCS, pp. 863-868. Springer (2013) |
| [37] | Colange, M., Baarir, S., Kordon, F., Thierry-Mieg, Y.: Towards distributed software model-checking using decision diagrams. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV’13), vol. 8044 of LNCS, pp. 830-845. Springer (2013) |
| [38] | Behrmann, G., Cougnard, A., David, A., Fleury, E., Guldstrand Larsen, K., Lime, D.: Uppaal-tiga: time for playing games! In: 19th International Conference on Computer Aided Verification, CAV’07, vol. 4590 of Lecture Notes in Computer Science, pp. 121-125. Springer (2007) · Zbl 1119.68005 |
| [39] | Barnat, J., Brim, L., Češka, M., Ročkai, P.: DiVinE: parallel distributed model checker (tool paper). In: Sharygina, N., Veith, H. (eds.) Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, pp. 4-7. IEEE (2010) |
| [40] | Holzmann, G .J.: The SPIN Model Checker—Primer and Reference Manual, 1st edn. Addison-Wesley, Reading (2004) |
| [41] | Blom, S., van de Pol, J., Weber, M.: Ltsmin: Distributed andsymbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, vol. 6174 of Lecture Notes in Computer Science, pp. 354-359. Springer, Berlin (2010) · Zbl 1267.68143 |
| [42] | Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools, 1st edn. Springer Publishing Company Incorporated, Berlin (2010) · Zbl 1002.68029 |
| [43] | Harrison, M.A.: Introduction to Formal Language Theory, 1st edn. Addison-Wesley Longman Publishing Co. Inc, Boston (1978) · Zbl 0411.68058 |
| [44] | Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal—a tool suite for automatic verification of real-time systems. In: Proceedings of Workshop on Verification and Control of Hybrid Systems III, Number 1066 in Lecture Notes in Computer Science, pp. 232-243. Springer (1995) |
| [45] | Millet, L., Potop-Butucaru, M., Sznajder, N., Tixeuil, S.: On the synthesis of mobile robots algorithms: the case of ring gathering. In: Proceedings of 16th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS’14), vol. 8756 of Lecture Notes in Computer Science, pp. 237-251. Springer (2014) · Zbl 1231.68164 |
| [46] | Ramadge, W.M., Wonham, P.J.: Supervisory control of a class of discrete event processes. In: Proceedings of 6th International Conference on Analysis and Optimization of Systems, vol. 63 of LNCS. Springer (1984) · Zbl 0556.93045 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
