Sciweavers

Share
ASM
2008
ASM

Using EventB to Create a Virtual Machine Instruction Set Architecture

8 years 10 months ago
Using EventB to Create a Virtual Machine Instruction Set Architecture
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 lored 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 g the MIDAS (Microprocessor Instruction and Data Abstraction System) VM, capable of running binary executables compiled from high-level s such as C [9]. The abstract model is incrementally refined to a model capable of automatic translation to ...
Stephen Wright
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ASM
Authors Stephen Wright
Comments (0)
books