The validation and implementation of real-time robotics systems using Cleopatra object-oriented physically-correct specifications

ABSTRACT

The specification of a real-time system is often the result of a process, whereby a conceptual control system is fleshed out as a computer program. To be accurate, this process must preserve important causal and structural properties of the control system. For example, if the control system has multiple functional components operating concurrently, then the process of mapping these components into a computer program executing on a single processor, must ensure that these components do not interact in ways that are physically impossible. In this paper we review our work on CLEOPATRA, an object oriented specification and programming language that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Unrealistic systems---possessing properties such as infinite capacities or perfect timing---cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle---not to mention the elimination of potential hazards that would have gone unnoticed.

REFERENCES

• 1: [1] R. Bajcsy. Perception with feedback. In Proceedings of the 1988 Darpa Image Understanding Workshop, 1988.
• 2: [2] Azer Bestavros. The Michael - Merlin Connection: Programming tools for the remote control of the American Cimflex robot. Robotics Laboratory, Harvard University, Cambridge, MA, September 1988.
• 3: [3] Azer Bestavros. TRA-based real-time executable specification using CLEOPATRA. In Proceedings of the 10th Annual Rochester Forth Conference on Embedded Systems , Rochester, NY, June 1990. (revised May 1991).
• 4: [4] Azer Bestavros. Planning for embedded systems: A real-time prospective. In Proceedings of AIRTC-91: The 3rd IFAC Workshop on Artificial Intelligence in Real Time Control, Napa/Sonoma Region, CA, September 1991.
• 5: [5] Azer Bestavros. Specification and verification or real-time embedded systems using the Time-constrained Reactive Automata. In Proceedings of RTSS'91: The 12th IEEE Real-time Systems Symposium, pages 244-253, San Antonio, Texas, December 1991.
• 6: Azer Bestavros, Time-constrained reactive automata: a novel development methodology for embedded real-time systems, Harvard University, Cambridge, MA, 1992
• 7: [7] Azer Bestavros. Cleopatra: Physically-correct specifications of embedded real-time programs. In Proceedings of the ACM SIGPLAN Workshop on Language, Compiler and Tool Support for Real-Time Systems, Orlando, FL, June 1994.
• 8: [8] Azer Bestavros. An ounce of prevention is worth a pound of cure: Towards physically-correct specifications of embedded real-time systems. In Proceedings of COMPASS'94: The Ninth Annual IEEE Conference on Computer Assurance, Gaithersburg, MD, June 1994.
• 9: [9] Azer Bestavros, James Clark, and Nicola Ferrier. Management of sensori-motor activity in mobile robots. In Proceedings of the 1990 IEEE International Conference on Robotics & Automation, Cincinati, Ohio, May 1990. IEEE Computer Society Press.
• 10: [10] Azer Bestavros, Devora Reich, and Robert Popp. CLEOPATRA compiler design and implementation. Technical Report TR-92-019, Computer Science Department, Boston University, Boston, MA, August 1992.
• 11: [11] Rodney A. Brooks. A robust layered control system for a mobile robot. IEEE Journal on Robotics and Automation , RA-2:14-23, April 1986.
• 12: Jen-Yao Chung , Jane W. S. Liu , Kwei-Jay Lin, Scheduling Periodic Jobs that Allow Imprecise Results, IEEE Transactions on Computers, v.39 n.9, p.1156-1174, September 1990 [doi>10.1109/12.57057]
• 13: [13] James Clark, Nicola Ferrier, and Lei Wang. A robotics system for manipulation using directed vision feedback. Internal report, Robotics laboratory, Harvard University, Cambridge, MA, 1991.
• 14: E Kligerman , A D Stoyenko, Real-time Euclid: a language for reliable real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.941-949, Sept. 1986
• 15: [15] Nancy Lynch and Mark Tuttle. An introduction to Input/Output Automata. Technical Report MIT/LCS/TM-373, MIT, Cambridge, Massachusetts, November 1988.
• 16: J. A. Stankovic , K. Ramamritham, The Spring kernel: a new paradigm for real-time operating systems, ACM SIGOPS Operating Systems Review, v.23 n.3, p.54-71, July 1989 [doi>10.1145/71021.71024]
• 17: Niklaus Wirth, Toward a discipline of real-time programming, Communications of the ACM, v.20 n.8, p.577-583, Aug. 1977 [doi>10.1145/359763.359798]
• 18: Pamela Zave, The operational versus the conventional approach to software development, Communications of the ACM, v.27 n.2, p.104-118, Feb. 1984 [doi>10.1145/69610.357982]

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.3 PROGRAMMING LANGUAGES

General Terms:
Design, Languages, Management