Formal verification of distributed dynamic thermal management

Muhammad Ismail, Osman Hasan, Thomas Ebi, Muhammad Shafique, Jorg Henkel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Simulation is the state-of-the-art analysis technique for distributed thermal management schemes. Due to the numerous parameters involved and the distributed nature of these schemes, such non-exhaustive verification may fail to catch functional bugs in the algorithm or may report misleading performance characteristics. To overcome these limitations, we propose a methodology to perform formal verification of distributed dynamic thermal management for many-core systems. The proposed methodology is based on the SPIN model checker and the Lamport timestamps algorithm. Our methodology allows specification and verification of both functional and timing properties in a distributed many-core system. In order to illustrate the applicability and benefits of our methodology, we perform a case study on a state-of-the-art agent-based distributed thermal management scheme.

Original languageEnglish (US)
Title of host publication2013 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2013 - Digest of Technical Papers
Pages248-255
Number of pages8
DOIs
StatePublished - 2013
Event2013 32nd IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2013 - San Jose, CA, United States
Duration: Nov 18 2013Nov 21 2013

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other2013 32nd IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2013
CountryUnited States
CitySan Jose, CA
Period11/18/1311/21/13

ASJC Scopus subject areas

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Formal verification of distributed dynamic thermal management'. Together they form a unique fingerprint.

Cite this