Predictable programs in barcodes

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

doi:10.1145/581630.581679

Predictable programs in barcodes

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02
Pages	298-303
Number of pages	6
DOIs	https://doi.org/10.1145/581630.581679
State	Published - 2002
Externally published	Yes
Event	2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02 - Grenoble, France Duration: Oct 8 2002 → Oct 11 2002

Publication series

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

Other

Other	2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02
Country/Territory	France
City	Grenoble
Period	10/8/02 → 10/11/02

Keywords

Active barcodes
Code delivery
Formal verification
Programmability of embedded devices

ASJC Scopus subject areas

Hardware and Architecture
Electrical and Electronic Engineering

Online availability

10.1145/581630.581679

Library availability

Discover UIUC Full Text

Cite this

Goodloe, A., McDougall, M., Gunter, C. A., & Alur, R. (2002). Predictable programs in barcodes. In Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02 (pp. 298-303). (Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02). https://doi.org/10.1145/581630.581679

Predictable programs in barcodes. / Goodloe, Alwyn; McDougall, Michael; Gunter, Carl A. et al.
Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02. 2002. p. 298-303 (Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Goodloe, A, McDougall, M, Gunter, CA & Alur, R 2002, Predictable programs in barcodes. in Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02. Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02, pp. 298-303, 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02, Grenoble, France, 10/8/02. https://doi.org/10.1145/581630.581679

Goodloe A, McDougall M, Gunter CA, Alur R. Predictable programs in barcodes. In Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02. 2002. p. 298-303. (Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02). doi: 10.1145/581630.581679

@inproceedings{d60333c0a5ec4b74b4961559b4905189,

title = "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.",

keywords = "Active barcodes, Code delivery, Formal verification, Programmability of embedded devices",

author = "Alwyn Goodloe and Michael McDougall and Gunter, {Carl A.} and Rajeev Alur",

year = "2002",

doi = "10.1145/581630.581679",

language = "English (US)",

isbn = "1581135750",

series = "Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02",

pages = "298--303",

booktitle = "Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02",

note = "2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02 ; Conference date: 08-10-2002 Through 11-10-2002",

}

TY - GEN

T1 - Predictable programs in barcodes

AU - Goodloe, Alwyn

AU - McDougall, Michael

AU - Gunter, Carl A.

AU - Alur, Rajeev

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - Active barcodes

KW - Code delivery

KW - Formal verification

KW - Programmability of embedded devices

UR - http://www.scopus.com/inward/record.url?scp=35248819810&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248819810&partnerID=8YFLogxK

U2 - 10.1145/581630.581679

DO - 10.1145/581630.581679

M3 - Conference contribution

AN - SCOPUS:35248819810

SN - 1581135750

SN - 9781581135756

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

SP - 298

EP - 303

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

T2 - 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES '02

Y2 - 8 October 2002 through 11 October 2002

ER -

Predictable programs in barcodes

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this