A Transformational Perspective into the Core of an Abstract Class Loader for the SSP

Victor L Winter, Jason Beranek, Fares Fraij, Steve Roach, Greg Wickstrom

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

The SSP is a hardware implementation of a subset of the JVM for use in high-consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP, as well as increasing its performance. Because of the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.

Original languageEnglish (US)
Pages (from-to)773-818
Number of pages46
JournalACM Transactions on Embedded Computing Systems
Volume5
Issue number4
DOIs
StatePublished - Jan 1 2006

Fingerprint

Loaders
Computer programming languages
Specifications
Hardware

Keywords

  • ACL2 Verification
  • HATS
  • Java Class Loader Strategic programming
  • Program Transformation
  • SSP
  • TL
  • higher-order rewriting

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Cite this

A Transformational Perspective into the Core of an Abstract Class Loader for the SSP. / Winter, Victor L; Beranek, Jason; Fraij, Fares; Roach, Steve; Wickstrom, Greg.

In: ACM Transactions on Embedded Computing Systems, Vol. 5, No. 4, 01.01.2006, p. 773-818.

Research output: Contribution to journalArticle

Winter, Victor L ; Beranek, Jason ; Fraij, Fares ; Roach, Steve ; Wickstrom, Greg. / A Transformational Perspective into the Core of an Abstract Class Loader for the SSP. In: ACM Transactions on Embedded Computing Systems. 2006 ; Vol. 5, No. 4. pp. 773-818.
@article{bf9bb722b1414e4290dc43ccadfb01bf,
title = "A Transformational Perspective into the Core of an Abstract Class Loader for the SSP",
abstract = "The SSP is a hardware implementation of a subset of the JVM for use in high-consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP, as well as increasing its performance. Because of the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.",
keywords = "ACL2 Verification, HATS, Java Class Loader Strategic programming, Program Transformation, SSP, TL, higher-order rewriting",
author = "Winter, {Victor L} and Jason Beranek and Fares Fraij and Steve Roach and Greg Wickstrom",
year = "2006",
month = "1",
day = "1",
doi = "10.1145/1196636.1196639",
language = "English (US)",
volume = "5",
pages = "773--818",
journal = "Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "4",

}

TY - JOUR

T1 - A Transformational Perspective into the Core of an Abstract Class Loader for the SSP

AU - Winter, Victor L

AU - Beranek, Jason

AU - Fraij, Fares

AU - Roach, Steve

AU - Wickstrom, Greg

PY - 2006/1/1

Y1 - 2006/1/1

N2 - The SSP is a hardware implementation of a subset of the JVM for use in high-consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP, as well as increasing its performance. Because of the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.

AB - The SSP is a hardware implementation of a subset of the JVM for use in high-consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP, as well as increasing its performance. Because of the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.

KW - ACL2 Verification

KW - HATS

KW - Java Class Loader Strategic programming

KW - Program Transformation

KW - SSP

KW - TL

KW - higher-order rewriting

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

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

U2 - 10.1145/1196636.1196639

DO - 10.1145/1196636.1196639

M3 - Article

VL - 5

SP - 773

EP - 818

JO - Transactions on Embedded Computing Systems

JF - Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 4

ER -