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 Scopus citations

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
Publication statusPublished - Jan 1 2006

    Fingerprint

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