Predictable programs in barcodes

ABSTRACT

We explore the challenges for making the programming interfaces for embedded devices open and safe, and present a prototype architecture for delivering verified programs using barcodes. In particular, we consider programs for microwave ovens, which provide a basic open API for controlling cooking times. In our architecture, recipes are written in Java, and their safety properties are formally verified using the model checker Spin. We use off-the-shelf utilities for compressing the byte code, and use two-dimensional barcodes for program delivery. We report on experiments that demonstrate the feasibility of the proposed architecture for predictability and delivery.

REFERENCES

• 1: I. 15417:2000. Automatic identification and data capture techniques - bar code symbology specification - code 128. Technical report, International Standards Organizatiopn, 2000.
• 2: I. 16388:1999. Automatic identification and data capture techniques -bar code symbology specifications -- code 39. Technical report, International Standards Organization, 1999.
• 3: Ken Arnold , James Gosling , David Holmes, The Java Programming Language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 4: A. BC11-ISS. Data matrix. Technical report, AIM, 1996.
• 5: A. BC13-ISS. Aztec code. Technical report, AIM, 1997.
• 6: G. Berry and G. Gonthier. The synchronous programming language esterel: design, semantics, implementation. Technical Report 842, INRIA, 1988.
• 7: D. M. C. Nevill-Manning, I.H. Witten. Compression by induction of hierarchial grammars. In J. A. Storer and M. Cohen, editors, Proceeding Data Compression Conference, pages 244--253. IEEE Press, 1994.
• 8: Edmund M. Clarke , Robert P. Kurshan, Computer-aided verification, IEEE Spectrum, v.33 n.6, p.61-67, June 1996 [doi>10.1109/6.499951]
• 9: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 10: U. C. Council. Ansi/ucc1-2000:u.p.c. symbol specification manual. Technical report, American National Standards Institute, 2000.
• 11: Conal Elliott , Paul Hudak, Functional reactive animation, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.263-273, June 09-11, 1997, Amsterdam, The Netherlands
• 12: Nicolas Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, Norwell, MA, 1992
• 13: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 14: Thomas Kistler , Michael Franz, A Tree-Based Alternative to Java Byte-Codes, International Journal of Parallel Programming, v.27 n.1, p.21-33, Feb. 1999 [doi>10.1023/A:1018740018601]
• 15: Lars Ræder Clausen , Ulrik Pagh Schultz , Charles Consel , Gilles Muller, Java bytecode compression for low-end embedded systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.3, p.471-489, May 2000 [doi>10.1145/353926.353933]
• 16: William Pugh, Compressing Java class files, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.247-258, May 01-04, 1999, Atlanta, Georgia, United States
• 17: C. Stork and V. Haldar. Compressed abstact syntax trees for mobile code. In Proceeding of Workshop on Intermediate Representation Engineering, 2001.
• 18: 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
• 19: J. Ziv and A. Lempel. Compression of individual sequences via variable-rate coding. IEEE Transactions Information Theory, 24(5):530--536, 1978.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures; Languages (e.g., description, interconnection, definition)
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Model checking
      D.2.7 Distribution, Maintenance, and Enhancement

General Terms:
Languages, Reliability, Verification

Keywords:
active barcodes, code delivery, formal verification, programmability of embedded devices