The Operational Semantics of a Java Secure Processor

Pieter H. Hartel; M.J. Butler; M. Levy

doi:10.1007/3-540-48737-9_9

The Operational Semantics of a Java Secure Processor

Pieter H. Hartel, M.J. Butler, M. Levy

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

165 Downloads (Pure)

Abstract

A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.

Original language	Undefined
Title of host publication	Formal Syntax and Semantics of Java
Editors	J. Alves-Foss
Place of Publication	Berlin
Publisher	Springer
Pages	313-352
Number of pages	40
ISBN (Print)	3-540-66158-1
DOIs	https://doi.org/10.1007/3-540-48737-9_9
Publication status	Published - 1999

Publication series

Name
Publisher	Springer-Verlag

Keywords

EWI-1037
IR-55694
SCS-Cybersecurity

Access to Document

10.1007/3-540-48737-9_9

http://www.springerlink.com/link.asp?id=emnvr5rvge2qardy

Cite this

@inbook{626d8515d45f480092d50f703da4049d,

title = "The Operational Semantics of a Java Secure Processor",

abstract = "A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.",

keywords = "EWI-1037, IR-55694, SCS-Cybersecurity",

author = "Hartel, {Pieter H.} and M.J. Butler and M. Levy",

note = "Imported from DIES",

year = "1999",

doi = "10.1007/3-540-48737-9_9",

language = "Undefined",

isbn = "3-540-66158-1",

publisher = "Springer",

pages = "313--352",

editor = "J. Alves-Foss",

booktitle = "Formal Syntax and Semantics of Java",

}

TY - CHAP

T1 - The Operational Semantics of a Java Secure Processor

AU - Hartel, Pieter H.

AU - Butler, M.J.

AU - Levy, M.

N1 - Imported from DIES

PY - 1999

Y1 - 1999

N2 - A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.

AB - A formal specification of a Java Secure Processor is presented, which is mechanically checked for type consistency, well formedness and operational conservativity. The specification is executable and it is used to animate and study the behaviour of sample Java programs. The purpose of the semantics is to document the behaviour of the complete JSP for the benefit of implementors.

KW - EWI-1037

KW - IR-55694

KW - SCS-Cybersecurity

U2 - 10.1007/3-540-48737-9_9

DO - 10.1007/3-540-48737-9_9

M3 - Chapter

SN - 3-540-66158-1

SP - 313

EP - 352

BT - Formal Syntax and Semantics of Java

A2 - Alves-Foss, J.

PB - Springer

CY - Berlin

ER -