{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T20:59:04Z","timestamp":1694638744738},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            The instruction set architecture (ISA) of a computing machine is the definition of the binary instructions, registers, and memory space visible to an executable binary image. ISAs are typically implemented in hardware as microprocessors, but also in software running on a host processor, i.e. virtual machines (VMs). Despite there being many ISAs 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 robust ISAs by the formal construction of all normal and exception conditions for each instruction. This is a task to which the Event-B (Metayer et\u00a0al. in Rodin deliverable 3.2 Event-B language,\n            <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"url\" xlink:href=\"http:\/\/rodin.cs.ncl.ac.uk\">http:\/\/rodin.cs.ncl.ac.uk<\/jats:ext-link>\n            , 2005; Schneider in The B-method an introduction, Palgrave, Basingstoke, 2001) formal notation is well suited. This paper describes a project to use the Rodin tool-set (Abrial in Formal methods and software engineering, Springer, Berlin, 2006) to perform such a process, ultimately producing two variants of the MIDAS (Microprocessor Instruction and Data Abstraction System) ISA (Wright in Abstract state machines, B and Z, Springer, Berlin, 2007; Wright in MIDAS machine specification, Bristol University,\n            <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"url\" xlink:href=\"http:\/\/www.cs.bris.ac.uk\/Publications\">http:\/\/www.cs.bris.ac.uk\/Publications<\/jats:ext-link>\n            , 2009) as VMs. The abstract model is incrementally refined to variant models capable of automatic translation to C source code, which this is compiled to create useable VMs. These are capable of running binary executables compiled from high-level languages such as C (Kernighan and Ritchie in The C programming language, Prentice-Hall, Englewood Cliffs, 1988), and compilers targeted to each variant allow demonstration programs to be executed on them.\n          <\/jats:p>","DOI":"10.1007\/s00165-009-0142-7","type":"journal-article","created":{"date-parts":[[2010,1,20]],"date-time":"2010-01-20T13:30:44Z","timestamp":1263994244000},"page":"73-89","source":"Crossref","is-referenced-by-count":3,"title":["Using Event-B to construct instruction set architectures"],"prefix":"10.1145","volume":"23","author":[{"given":"Stephen","family":"Wright","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Bristol, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Bristol, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R (1996) The B-Book: assigning programs to meanings","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Butler M Hallerstede S Voisin L (2006) An open extensible tool environment for Event-B. In: Formal methods and software engineering. Springer Berlin","DOI":"10.1007\/11901433_32"},{"key":"e_1_2_1_2_3_2","unstructured":"AMD Inc (2007) 128-Bit SSE5 instruction set"},{"key":"e_1_2_1_2_4_2","unstructured":"B-Core (2006) The B-toolkit user manual. B-Core (UK) Ltd"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Beer I Ben-David S (1997) RuleBase: model checking at IBM. CAV","DOI":"10.1007\/3-540-63166-6_53"},{"key":"e_1_2_1_2_6_2","unstructured":"Brock B Hunt W (1991) Report on the formal specification and partial verification of the VIPER microprocessor. In: Proceedings of the sixth annual conference on computer assurance systems integrity software safety and process security"},{"key":"e_1_2_1_2_7_2","unstructured":"Butler M (2006) Rodin deliverable D16 prototype plug-in tools. http:\/\/rodin.cs.ncl.ac.uk"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Caset L (2002) Formal development of an embedded verifier for Java card byte code. In: International conference on dependable systems and networks","DOI":"10.1007\/3-540-45614-7_17"},{"key":"e_1_2_1_2_9_2","unstructured":"Eclipse (2009) Eclipse platform homepage. http:\/\/www.eclipse.org\/"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Evans N Butler M (2006) A proposal for records in Event-B. In: Formal methods 2006","DOI":"10.1007\/11813040_16"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Evans N Grant N (2007) Towards the formal verification of a Java processor in Event-B. In: Proceedings of the BAC-FACS refinement workshop","DOI":"10.1016\/j.entcs.2008.02.015"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Fox A (2003) Formal specification and verification of ARM6. In: Theorem proving in higher order logics. Springer Berlin","DOI":"10.1007\/10930755_2"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Graham B Birtwistle G (1990) Formalising the design of an SECD chip. In: Hardware specification verification and synthesis: mathematical aspects. Springer Berlin","DOI":"10.1007\/0-387-97226-9_23"},{"key":"e_1_2_1_2_14_2","volume-title":"Computer architecture, a quantitive approach","author":"Hennessy J","year":"2003"},{"key":"e_1_2_1_2_15_2","unstructured":"Hitachi Ltd (1998) SH7707 hardware manual"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hunt W (1994) FM8501: A verified microprocessor. In: Lecture notes in artificial intelligence subseries of lecture notes in computer science. Springer Berlin","DOI":"10.1007\/3-540-57960-5"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/100511"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Klein G Nipkow T (2001) Verified bytecode verifiers. In: Foundations of software science and computation structures. Springer Berlin","DOI":"10.1007\/3-540-45315-6_23"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","DOI":"10.1109\/9780470544433","volume-title":"DSP processor fundamentals","author":"Lapsley P","year":"1997"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Lee E (1989) Programmable DSP processors part I and II. IEEE ASSP Mag Oct 1988 Jan 1989","DOI":"10.1109\/53.16934"},{"key":"e_1_2_1_2_21_2","volume-title":"ProB: a model checker for B. FME 2003","author":"Leuschel M","year":"2003"},{"key":"e_1_2_1_2_22_2","unstructured":"Lindholm T Yellin F (1999) The Java virtual machine specification 2nd edn."},{"key":"e_1_2_1_2_23_2","unstructured":"Metayer C Abrial J-R Voisin L (2005) Rodin deliverable 3.2 Event-B language. http:\/\/rodin.cs.ncl.ac.uk"},{"key":"e_1_2_1_2_24_2","unstructured":"Patterson D (2007) Computer organization and design: the hardware\/software interface. Morgan Kaufmann Menlo Park"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Qian Z (1999) A formal specification of Java virtual machine instructions for objects methods and subroutines. In: Formal syntax and semantics of Java. Springer Berlin","DOI":"10.1007\/3-540-48737-9_8"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/861881"},{"issue":"14","key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","first-page":"1475","DOI":"10.1002\/spe.812","article-title":"Practical testing of a C99 compiler using output comparison","volume":"37","author":"Sherridan F","year":"2007","journal-title":"Softw Pract Experience"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/61690"},{"key":"e_1_2_1_2_29_2","volume-title":"Formal verification of an avionics microprocessor","author":"Srivas M","year":"1995"},{"key":"e_1_2_1_2_30_2","unstructured":"Stallman R (2001) Using and porting the GNU compiler collection. In: Free Software Foundation"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/559207"},{"key":"e_1_2_1_2_32_2","volume-title":"Practical model-based testing\u2014a tools approach","author":"Utting M","year":"2007"},{"key":"e_1_2_1_2_33_2","unstructured":"Wright S (2009) MIDAS machine specification. Bristol University. http:\/\/www.cs.bris.ac.uk\/Publications"},{"key":"e_1_2_1_2_34_2","unstructured":"Wright S (2009) Automatic generation of C from Event-B. In: Workshop on integration of model-based formal methods and tools"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0142-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0142-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0142-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:36Z","timestamp":1641484536000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0142-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1007\/s00165-009-0142-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0142-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]}}}