Industrial deployment of system engineering methods providing high dependability and productivity


MIDAS: A Formally Constructed Virtual Machine

Wright, Stephen (2009) MIDAS: A Formally Constructed Virtual Machine. [DEPLOY Interest Group Item] (Unpublished)

[img]ZIP Archive (WinRar bundle of enclosed zip/rar files.) - Supplemental Material
PDF (Description and installation instructions) - Submitted Version


MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of defined instructions, in order to make complete refinement practical. The intention is to simplify the number and complexity of the defined instructions at the cost of compiler complexity, run-time performance and code density, without compromising representativeness. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.

Item Type:DEPLOY Interest Group Item
Uncontrolled Keywords:Event-B Virtual Machine Instruction Set Architecture
Subjects:Event-B > Event-B Examples
ID Code:84
Deposited By:Mr Stephen Wright
Deposited On:06 Jun 2009 11:51
Last Modified:19 Apr 2010 16:05

Repository Staff Only: item control page

Deploy-Project - All right reserved