Using EventB to Create a Virtual Machine Instruction Set Architecture

Wright Steve

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

1 Citation (Scopus)
1 Downloads (Pure)

Abstract

A Virtual Machine (VM) is a program running on a conventional microprocessor that emulates the binary instruction set, registers, and memory space of an idealized computing machine, a well-known example being the Java Virtual Machine (JVM). Despite there being many binary Instruction Set Architectures (ISA) in existence, all share a set of core properties which have been tailored to their particular applications. An abstract model may capture these generic properties and be subsequently refined to a particular machine, providing a reusable template for development of formally proven ISAs: this is a task to which the EventB [16,18] notation is well suited. This paper describes a project to use the RODIN tool-set [24] to perform such a process, ultimately producing the MIDAS (Microprocessor Instruction and Data Abstraction System) VM, capable of running binary executables compiled from high-level languages such as C [9]. The abstract model is incrementally refined to a model capable of automatic translation to C source code, and compilation for a hardware platform using a standard compiler. A second C compiler, targeted to the VM itself, allows C programs to be executed on it.
Translated title of the contributionUsing EventB to Create a Virtual Machine Instruction Set Architecture
Original languageEnglish
Title of host publicationAbstract State Machines, B and Z
Subtitle of host publicationFirst International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings
PublisherSpringer Berlin Heidelberg
Pages265-279
Number of pages15
ISBN (Electronic)9783540876038
ISBN (Print)9783540876021
DOIs
Publication statusPublished - 16 Sep 2008

Publication series

NameLecture Notes in Computer Science
Volume5238

Bibliographical note

ISBN: 0302974316113349
Publisher: Springer Berlin / Heidelberg
Name and Venue of Conference: Abstract State Machines, B and Z
Other identifier: 2000957

Fingerprint Dive into the research topics of 'Using EventB to Create a Virtual Machine Instruction Set Architecture'. Together they form a unique fingerprint.

Cite this