Formal probabilistic analysis of distributed dynamic thermal management

Shafaq Iqtedar, Osman Hasan, Muhammad Shafique, Jorg Henkel

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

Abstract

The prevalence of Dynamic Thermal Management (DTM) schemes coupled with demands for high reliability motivate the rigorous verification and testing of these schemes before deployment. Conventionally, these schemes are analyzed using either simulations or by running on real systems. But these traditional analysis techniques cannot exhaustively validate the distributed DTM schemes and thus compromise on the accuracy of the analysis results. Moreover, the randomness due to task assignments, task completion times and re-mappings, is often ignored in the analysis of distributed DTM schemes. We propose to overcome both of these limitations by using probabilistic model checking, which is a formal method for modeling and verifying concurrent systems with randomized behaviors. The paper presents a case study on the formal verification of a state-of-the-art distributed DTM scheme using the PRISM model checker.

Original languageEnglish (US)
Title of host publicationProceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1221-1224
Number of pages4
ISBN (Electronic)9783981537048
DOIs
StatePublished - Apr 22 2015
Event2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015 - Grenoble, France
Duration: Mar 9 2015Mar 13 2015

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
Volume2015-April
ISSN (Print)1530-1591

Other

Other2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015
CountryFrance
CityGrenoble
Period3/9/153/13/15

ASJC Scopus subject areas

  • Engineering(all)

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

Cite this