Predictable programs in barcodes

Alwyn Goodloe, Michael McDougall, Carl A. Gunter, Rajeev Alur

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02
Pages298-303
Number of pages6
DOIs
StatePublished - 2002
Event2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02 - Grenoble, France
Duration: Oct 8 2002Oct 11 2002

Publication series

NameProceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02

Other

Other2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02
CountryFrance
CityGrenoble
Period10/8/0210/11/02

Keywords

  • Active barcodes
  • Code delivery
  • Formal verification
  • Programmability of embedded devices

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Predictable programs in barcodes'. Together they form a unique fingerprint.

Cite this