A Case Study in Specifying and Testing Architectural Features
P. Krishnan
Department of Computer Science
University of Canterbury
Abstract
This paper studies the specification and testing of two main architectural features. We consider restricted forms of instruction pipelining and parallel memory models present in the SPARC specification. The feasibility of using an automatic tool, the concurrency work bench, has been demonstrated.
Keywords Architecture, SPARC, specification, verification, CCS, modal logic, concurrency work bench