• Information Technology
  • Human Resources
  • Careers
  • Giving
  • Library
  • Bookstore
  • Active Living
  • Continuing Education
  • Go Dinos
  • UCalgary Maps
  • UCalgary Directory
  • Academic Calendar
My UCalgary
Webmail
D2L
ARCHIBUS
IRISS
  • Faculty of Arts
  • Cumming School of Medicine
  • Faculty of Environmental Design
  • Faculty of Graduate Studies
  • Haskayne School of Business
  • Faculty of Kinesiology
  • Faculty of Law
  • Faculty of Nursing
  • Faculty of Nursing (Qatar)
  • Schulich School of Engineering
  • Faculty of Science
  • Faculty of Social Work
  • Faculty of Veterinary Medicine
  • Werklund School of Education
  • Information TechnologiesIT
  • Human ResourcesHR
  • Careers
  • Giving
  • Library
  • Bookstore
  • Active Living
  • Continuing Education
  • Go Dinos
  • UCalgary Maps
  • UCalgary Directory
  • Academic Calendar
  • Libraries and Cultural Resources
View Item 
  •   PRISM Home
  • Science
  • Science Research & Publications
  • View Item
  •   PRISM Home
  • Science
  • Science Research & Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

AMULET1: SPECIFICATION AND VERIFICATION IN CCS

Thumbnail
Download
1995-573-25.pdf (14.11Mb)
Download Record
Download to EndNote/RefMan (RIS)
Download to BibTex
Author
Liu, Ying
Accessioned
2008-05-20T23:31:47Z
Available
2008-05-20T23:31:47Z
Computerscience
1999-05-27
Issued
1995-09-01
Subject
Computer Science
Type
unknown
Metadata
Show full item record

Abstract
There has been a dramatic resurgence of asynchronous hardware designs in recent years. Since state spaces multiply, asynchronous systems can be extremely state rich and it is correspondingly difficult to reason about their characteristic properties with the traditional techniques of simulation. The alternative, adopted here, is to use formal techniques of specification and property checking to reason about asynchronous designs and to test them thoroughly for desired behaviours. This dissertation explores the feasibility of applying the CCS process algebra and its supporting tool, the Edinburgh Concurrency Workbench (CWB), to the formal specification and verification of a specific asynchronous microprocessor (AMULET1) developed by the AMULET group at Manchester University. AMULET1 is modeled at both the system level and the floor plan level. The system level model shows how each instruction class flows through the major components of the processor, and can be used outwards in modeling embedded applications and inwards to document the roles of the floor plan elements. The subsystem level modeling presents register transfer level detail of the floor plan elements and serves as an implementation guide to designers. This is the first attempt to apply formal techniques to a full scale, practical, industrial-strength asynchronous design. CCS is demonstrated to be an appropriate and efficient notation for modeling such complex designs. In the main, property checking on the CWB proved to be a reliable and robust way of detecting and repairing specification flaws. Although this work is \fIpost facto\fR, it suggests that the systematic incorporation of formal specification and verification techniques into the design cycle could shorten the overall design window and help reduce fabrication iterations.
Notes
We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.ca
Corporate
University of Calgary
Faculty
Science
Doi
http://dx.doi.org/10.11575/PRISM/31270
Uri
http://hdl.handle.net/1880/46560
Collections
  • Science Research & Publications

Browse

All of PRISMCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

My Account

LoginRegister

Download Results

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors

  • Email
  • SMS
  • 403.220.8895
  • Live Chat

Energize: The Campaign for Eyes High

Privacy Policy
Website feedback

University of Calgary
2500 University Drive NW
Calgary, AB T2N 1N4
CANADA

Copyright © 2017