Towards resource-certified software: a formal cost model for time and its application to an image-processing example

ABSTRACT

Visual tracking requires sophisticated algorithms working in real-time, and often space-limited, settings. While the input streams may be regular in structure, the algorithms are not, and must often deal with probabilistic metrics. To ensure progress in algorithm design without incurring excessive development costs, we propose a high-level programming approach married with predictable and compositional performance metrics. This enables the combination of independently developed program components into coherent software architecture, with certified resource use guarantee. Here, we present our approach and discuss its application to the development and resource analysis of a space bound mean shift algorithm for motion tracking, using the new embedded system-oriented language Hume.

REFERENCES

• 1: T. Amtoft, F. Nielson, and H. Nielson. Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, 1999.
• 2: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 3: D. Aspinall, L. Beringer, M. Hofmann, H.-W. Loidl, and A. Momigliano. A Resource-aware Program Logic for Grail. In Proc. ESOP'04 --- European Symposium on Programming, 2004.
• 4: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 5: R. Bird. Constructive Functional Programming. In STOP Summer School on Constructive Algorithmics, Abeland, 1989.
• 6: R. Burstall. Inductively Defined Functions in Functional Programming Languages. Technical Report ECS-LFCS-87-25, 1987.
• 7: K. Claessen and M. Sheeran. A Tutorial on Lava: a Hardware Desc. and Verification System. Aug. 2000.
• 8: Dorin Comaniciu , Peter Meer, Mean Shift: A Robust Approach Toward Feature Space Analysis, IEEE Transactions on Pattern Analysis and Machine Intelligence, v.24 n.5, p.603-619, May 2002 [doi>10.1109/34.1000236]
• 9: Dorin Comaniciu , Visvanathan Ramesh , Peter Meer, Kernel-Based Object Tracking, IEEE Transactions on Pattern Analysis and Machine Intelligence, v.25 n.5, p.564-575, May 2003 [doi>10.1109/TPAMI.2003.1195991]
• 10: Christian Ferdinand , Reinhold Heckmann , Marc Langenbach , Florian Martin , Michael Schmidt , Henrik Theiling , Stephan Thesing , Reinhard Wilhelm, Reliable and Precise WCET Determination for a Real-Life Processor, Proceedings of the First International Workshop on Embedded Software, p.469-485, October 08-10, 2001
• 11: Christian Ferdinand , Florian Martin , Reinhard Wilhelm , Martin Alt, Cache behavior prediction by abstract interpretation, Science of Computer Programming, v.35 n.2-3, p.163-189, Nov.1.1999 [doi>10.1016/S0167-6423(99)00010-6]
• 12: R. Fisher. CAVIAR: Context Aware Vision using Image-based Active Recognition, http://homepages.inf.ed.ac.uk/rbf/caviar/, 2005.
• 13: Kevin Hammond , Greg Michaelson, Hume: a domain-specific language for real-time embedded systems, Proceedings of the 2nd international conference on Generative programming and component engineering, p.37-56, September 22-25, 2003, Erfurt, Germany
• 14: K. Hammond and G. Michaelson. Predictable Space Behaviour in FSM-Hume. In Proc. Implementation of Functional Langs. (IFL '02), Madrid, Spain, Springer-Verlag LNCS 2670, 2003.
• 15: J. Hawkins and A. Abdallah. Behavioural Synthesis of a Parallel Hardware JPEG Decoder from a Functitonal Specification. In Proc. EuroPar 2002, Aug. 2002.
• 16: Martin Hofmann, A type system for bounded space and functional in-place update, Nordic Journal of Computing, v.7 n.4, p.258-289, Winter 2000
• 17: Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
• 18: M. Hofmann and S. Jost. Type-based amortised heap-space analysis. In Proc. ESOP 2006 - 2006 European Symp. on Programming, pages 22--37, 2006.
• 19: John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
• 20: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 21: John Matthews , Byron Cook , John Launchbury, Microprocessor Specification in Hawk, Proceedings of the 1998 International Conference on Computer Languages, p.90, May 14-16, 1998
• 22: S. Jost. Linearly Bounded Heap Space Analysis, Ludwig-Maximilians-Universität, München, Germany (in preparation). PhD thesis, 2006.
• 23: Marc Langenbach , Stephan Thesing , Reinhold Heckmann, Pipeline Modeling for Timing Analysis, Proceedings of the 9th International Symposium on Static Analysis, p.294-309, September 17-20, 2002
• 24: S.-C. Mu and R. S. Bird. Rebuilding a Tree from its Traversals: A Case Study of Program Inversion. In Proc. Australian Conf. on Prog. Lang. and Systems (APLAS 2003), pages 265--282, 2003.
• 25: J. Nordlander, M. Carlsson, and M. Jones. Programming with Time-Constrained Reactions (unpublished report). http://www.cse.ogi.edu/pacsoft/projects/Timber/publications.htm. 2006.
• 26: J. Nyström, P. Trinder, and D. King. High-level distribution for the rapid production of robust telecoms software: comparing c++ and erlang. Concurrency and Computation: Practice & Experience., 18, December 2006.
• 27: A. Rebón Portillo, K. Hammond, H.-W. Loidl, and P. Vasconcelos. A Sized Time System for a Parallel Functional Language (Revised). In Proc. Implementation of Functional Langs. (IFL '02), Madrid, Spain, Springer-Verlag LNCS 2670, 2003.
• 28: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 29: D. A. Turner, Elementary Strong Functional Programming, Proceedings of the First International Symposium on Functional Programming Languages in Education, p.1-13, December 04-06, 1995
• 30: D. Turner. Total Functional Programming. Journal of Universal Computing, 10(7):751--768, 2004.
• 31: L. Unnikrishnan, S. Stoller, and Y. Liu. Automatic Accurate Stack Space and Heap Space Analysis for High-Level Languages. Tech. Report 538, Comp. Sci. Dept., Indiana University, Apr. 2000.
• 32: P. Vasconcelos and K. Hammond. Inferring Costs for Recursive, Polymorphic and Higher-Order Functional Programs. In Proc. Implementation of Functional Languages (IFL 2003), 2004.
• 33: Malcolm Wallace , Colin Runciman, Extending a functional programming system for embedded applications, Software—Practice & Experience, v.25 n.1, p.73-96, Jan. 1995 [doi>10.1002/spe.4380250105]
• 34: Zhanyong Wan , Walid Taha , Paul Hudak, Real-time FRP, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, September 03-05, 2001, Florence, Italy

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods
      D.2.8 Metrics
          Subjects: Performance measures; Complexity measures

Keywords:
embedded systems, functional programming, motion tracking, resource bounds