Probabilistic formal verification methodology for decentralized thermal management in on-chip systems

Shafaq Iqtedar, Osman Hasan, Muhammad Shafique, Jörg Henkel

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

Abstract

Just like any other algorithm, Dynamic Thermal Management(DTM) schemes for multi-core architectures are susceptible to errors. Moreover, due to the wide spread usage and safety-critical nature of these schemes, there is a key demand for robust verification of these schemes before deployment. Traditional analysis techniques, like simulation and emulation, are inherently incomplete and therefore they cannot guarantee a complete absence of bugs. In this paper, we present a generic formal verification methodology, based of probabilistic model checking, for verifying decentralized DTM schemes. The paper provides a general modelling approach for developing a Markova model of any decentralized DTM scheme. Moreover, we identify a set of generic probabilistic properties that can be of an interest to DTM scheme designers. For illustration purposes, the proposed methodology is used to verify Thermal Aware Agent Based Power Economy (TAPE), which is a state-of-the-art decentralized DTM scheme.

Original languageEnglish (US)
Title of host publicationProceedings - 2015 IEEE 24th International Conference on Enabling Technologies
Subtitle of host publicationInfrastructures for Collaborative Enterprises, WETICE 2015
EditorsSumitra M. Reddy
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages210-215
Number of pages6
ISBN (Electronic)9781467376921
DOIs
StatePublished - Aug 12 2015
Event2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015 - Larnaca, Cyprus
Duration: Jun 15 2015Jun 17 2015

Publication series

NameProceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015

Conference

Conference2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015
CountryCyprus
CityLarnaca
Period6/15/156/17/15

Keywords

  • Approximate model checking
  • Decentralized dtm scheme
  • Many core system
  • Markov chain
  • Model checking
  • Power trading agent
  • Power unit
  • Probabilistic model checking
  • Tape dtm scheme
  • Temperature
  • Thermal hotspot

ASJC Scopus subject areas

  • Management Information Systems
  • Computer Networks and Communications
  • Computer Science Applications
  • Information Systems

Fingerprint Dive into the research topics of 'Probabilistic formal verification methodology for decentralized thermal management in on-chip systems'. Together they form a unique fingerprint.

Cite this