StarL: Towards a Unified Framework for Programming, Simulating and Verifying Distributed Robotic Systems

Abstract

We developed StarL as a framework for programming, simulating, and verifying distributed systems that interacts with physical processes. StarL framework has (a) a collection of distributed primitives for coordination, such as mutual exclusion, registration and geocast that can be used to build sophisticated applications, (b) theory libraries for verifying StarL applications in the PVS theorem prover, and (c) an execution environment that can be used to deploy the applications on hardware or to execute them in a discrete event simulator. The primitives have (i) abstract, nondeterministic specifications in terms of invariants, and assume-guarantee style progress properties, (ii) implementations in Java/Android that always satisfy the invariants and attempt progress using best effort strategies. The PVS theories specify the invariant and progress properties of the primitives, and have to be appropriately instantiated and composed with the application's state machine to prove properties about the application. We have built two execution environments: one for deploying applications on Android/iRobot Create platform and a second one for simulating large instantiations of the applications in a discrete even simulator. The capabilities are illustrated with a StarL application for vehicle to vehicle coordination in an automatic intersection that uses primitives for point-to-point motion, mutual exclusion, and registration.

References

1. The StarL framework, February 2015. Available for download from https://github.com/lin187/StarL_LCTES.
2. P. A. Abdulla and B. Jonsson. Verifying networks of timed processes. In Tools and Algorithms for the Construction and Analysis of Systems, pages 298--312. Springer, 1998.
3. M. Archer. TAME: PVS Strategies for special purpose theorem proving. Annals of Mathematics and Artificial Intelligence, 29(1/4), February 2001.
4. M. Archer, H. Lim, N. Lynch, S. Mitra, and S. Umeno. Specifying and proving properties of timed I/O automata in the TIOA toolkit. In MEMOCODE'06. IEEE, 2006.
5. M. Archer, H. Lim, N. Lynch, S. Mitra, and S. Umeno. Specifying and proving properties of timed I/O automata using Tempo. Design Automation for Embedded Systems, 2008.
6. C. Auger, Z. Bouzid, P. Courtieu, S. Tixeuil, and X. Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In Stabilization, Safety, and Security of Distributed Systems, volume 8255, pages 178--190. 2013.
7. G. Berry and L. Cosserat. The esterel synchronous programming language and its mathematical semantics. In Seminar on Concurrency, Carnegie-Mellon University, pages 389--448, London, UK, UK, 1985. Springer-Verlag.
8. J. Cortes, , S. Martinez, T. Karatas, and F. Bullo. Coverage control for mobile sensing networks. IEEE Transactions on Robotics and Automation, 20(2):243--255, 2004.
9. G. Coulouris, J. Dollimore, T. Kindberg, and G. Blair. Distributed Systems: Concepts and Design. Addison-Wesley Publishing Company, USA, 5th edition, 2011.
10. P. Courtieu, L. Rieg, S. Tixeuil, and X. Urbain. Impossibility of gathering, a certification. Information Processing Letters, 115(3):447 -- 452, 2015.
11. X. Défago and A. Konagaya. Circle formation for oblivious anonymous mobile robots with no common sense of orientation. In Proc. 2nd Int'l Workshop on Principles of Mobile Computing (POMC'02), pages 97--104, Toulouse, France, October 2002. ACM.
12. C. Dixon, R. Mahajan, S. Agarwal, A. Brush, B. Lee, S. Saroiu, and P. Bahl. An operating system for the home. In NSDI. USENIX, April 2012.
13. S. Dolev. Self-stabilization. MIT Press, Cambridge, MA, USA, 2000.
14. P. S. Duggirala, T. T. Johnson, A. Zimmerman, and S. Mitra. Static and dynamic analysis of timed distributed traces. In RTSS, pages 173--182, 2012.
15. P. Flocchini, G. Prencipe, N. Santoro, and P. Widmayer. Pattern formation by autonomous robots without chirality. In SIROCCO, pages 147--162, June 2001.
16. S. Gilbert, N. Lynch, S. Mitra, and T. Nolte. Self-stabilizing robot formations over unreliable networks. Special Issue on Self-adaptive and Self-organizing Wireless Networking Systems of ACM Transactions on Autonomous and Adaptive Systems (TAAS), 4(3):1--29, 2009.
17. M. R. Hafner, D. Cunningham, L. Caminiti, and D. D. Vecchio. Cooperative collision avoidance at intersections: Algorithms and experiments. IEEE Transactions on Intelligent Transportation Systems, 14(3):1162--1175, 2013.
18. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. In Proceedings of the IEEE, pages 1305--1320, 1991.
19. T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Decomposing refinement proofs using assume-guarantee reasoning. In Proceedings of the 2000 IEEE/ACM International Conference on Computer-aided Design, ICCAD '00, pages 245--253, Piscataway, NJ, USA, 2000. IEEE Press.
20. T. Johnson and S. Mitra. Parameterized verification of distributed cyber-physical systems:an aircraft landing protocol case study. In ACM/IEEE Third International Conference on Cyber-Physical Systems, April 2012, Beijing, China, 2012.
21. T. Johnson, S. Mitra, and K. Manamcheri. Safe and stabilizing distributed cellular flows. In Proceedings of IEEE Internaitonal Conference on Distributed Computing Systems (ICDCS 2010), 2010.
22. D. K. Kaynar, N. Lynch, R. Segala, and F. Vaandrager. The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science. Morgan Claypool, November 2005. Also available as Technical Report MIT-LCS-TR-917.
23. P. Krcál and W. Yi. Communicating timed automata: The more synchronous, the more difficult to verify. In Computer Aided Verification, 18th International Conference, CAV, volume 4144 of Lecture Notes in Computer Science, pages 249--262. Springer, 2006.
24. P. Le Guernic, A. Benveniste, P. Bournai, and T. Gautier. Signal--a data flow-oriented language for signal processing. Acoustics, Speech and Signal Processing, IEEE Transactions on, 34(2):362--374, 1986.
25. Q. Lindsey, D. Mellinger, and V. Kumar. Construction with quadrotor teams. Auton. Robots, 33(3):323--336, 2012.
26. Q. Lindsey, D. Mellinger, and V. Kumar. Construction with quadrotor teams. Autonomous Robots, 33(3):323--336, 2012.
27. S. Loos, A. Platzer, and L. Nistor. Adaptive cruise control: Hybrid, distributed, and now formally verified. In FM 2011: Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 42--56. Springer Berlin Heidelberg, 2011.
28. M. R. Lucas and D. M. Tilbury. A study of current logic design practices in the automotive manufacturing industry. Int. J. Hum.-Comput. Stud., 59(5):725--753, 2003.
29. M. Mesbahi and M. Egerstedt. Graph-theoretic Methods in Multiagent Networks. Princeton University Press.
30. N. Michael, D. Mellinger, Q. Lindsey, and V. Kumar. The grasp multiple micro-uav testbed. Robotics & Automation Magazine, IEEE, 17(3):56--65, 2010.
31. L. Millet, M. Potop-Butucaru, N. Sznajder, and S. Tixeuil. On the synthesis of mobile robots algorithms: The case of ring gathering. In Stabilization, Safety, and Security of Distributed Systems, volume 8756, pages 237--251. Springer International Publishing, 2014.
32. S. Mitra. A Verification Framework for Hybrid Systems. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA 02139, September 2007.
33. R. Olfati-Saber, J. Fax, and R. Murray. Consensus and cooperation in networked multi-agent systems. Proceedings of the IEEE, 95(1):215--233, January 2007.
34. R. Oung and R. DAndrea. The distributed flight array. Mechatronics, 21(6):908--917, 2011.
35. S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Computer-Aided Verification, CAV '96, number 1102 in LNCS, pages 411--414, New Brunswick, NJ, July/August 1996. Springer-Verlag.
36. S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999.
37. A. Platzer. Differential logic for reasoning about hybrid systems. In A. Bemporad, A. Bicchi, and G. C. Buttazzo, editors, HSCC, volume 4416 of Lecture Notes in Computer Science, pages 746--749. Springer, 2007.
38. A. Platzer. Quantified differential dynamic logic for distributed hybrid systems. In Computer Science Logic, volume 6247, pages 469--483. Springer Berlin Heidelberg, 2010.
39. G. Prencipe. Corda: Distributed coordination of a set of autonomous mobile robots. In ERSADS, pages 185--190, May 2001 2001.
40. M. Quigley, K. Conley, B. P. Gerkey, J. Faust, T. Foote, J. Leibs, R. Wheeler, and A. Y. Ng. Ros: an open-source robot operating system. In ICRA Workshop on Open Source Software, 2009.
41. M. Schwager, J. McLurkin, and D. Rus. Distributed coverage control with sensory feedback for networked robots. In Robotics: Science and Systems, Philadelphia, Pennsylvania, August 2006. The MIT Press.
42. C. Steiner. Bot in the delivery:kiva systems. Forbes Magazine, March 2009. http://www.forbes.com/forbes/2009/0316/040_bot_time_saves_nine.html.
43. W. Steiner and B. Dutertre. Automated formal verification of the TTEthernet synchronization quality. In NASA Formal Methods - Third International Symposium, NFM, volume 6617 of Lecture Notes in Computer Science, pages 375--390. Springer, 2011.
44. I. Suzuki and M. Yamashita. Distributed autonomous mobile robots: Formation of geometric patterns. SIAM Journal of computing, 28(4):1347--1363, 1999.
45. M. Turpin, K. Mohta, N. Michael, and V. Kumar. Goal assignment and trajectory planning for large teams of interchangeable robots. Auton. Robots, 37(4):401--415, 2014.
46. A. Zimmerman. Starl for programming reliable robotic networks. Master's thesis, University of Illinois at Urbana-Champaign, 2013.

Index Terms

• Computing methodologies

  • Distributed computing methodologies

    • Distributed programming languages

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language types

        • Distributed programming languages

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification