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

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

doi:10.1109/WETICE.2015.39

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

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

Electrical Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies
Subtitle of host publication	Infrastructures for Collaborative Enterprises, WETICE 2015
Editors	Sumitra M. Reddy
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	210-215
Number of pages	6
ISBN (Electronic)	9781467376921
DOIs	https://doi.org/10.1109/WETICE.2015.39
State	Published - Aug 12 2015
Event	2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015 - Larnaca, Cyprus Duration: Jun 15 2015 → Jun 17 2015

Publication series

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

Conference

Conference	2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015
Country/Territory	Cyprus
City	Larnaca
Period	6/15/15 → 6/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

Access to Document

10.1109/WETICE.2015.39

Cite this

Iqtedar, S., Hasan, O., Shafique, M., & Henkel, J. (2015). Probabilistic formal verification methodology for decentralized thermal management in on-chip systems. In S. M. Reddy (Ed.), Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015 (pp. 210-215). Article 7194362 (Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/WETICE.2015.39

Probabilistic formal verification methodology for decentralized thermal management in on-chip systems. / Iqtedar, Shafaq; Hasan, Osman; Shafique, Muhammad et al.
Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015. ed. / Sumitra M. Reddy. Institute of Electrical and Electronics Engineers Inc., 2015. p. 210-215 7194362 (Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Iqtedar, S, Hasan, O, Shafique, M & Henkel, J 2015, Probabilistic formal verification methodology for decentralized thermal management in on-chip systems. in SM Reddy (ed.), Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015., 7194362, Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015, Institute of Electrical and Electronics Engineers Inc., pp. 210-215, 2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015, Larnaca, Cyprus, 6/15/15. https://doi.org/10.1109/WETICE.2015.39

Iqtedar S, Hasan O, Shafique M, Henkel J. Probabilistic formal verification methodology for decentralized thermal management in on-chip systems. In Reddy SM, editor, Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015. Institute of Electrical and Electronics Engineers Inc. 2015. p. 210-215. 7194362. (Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015). doi: 10.1109/WETICE.2015.39

Iqtedar, Shafaq ; Hasan, Osman ; Shafique, Muhammad et al. / Probabilistic formal verification methodology for decentralized thermal management in on-chip systems. Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015. editor / Sumitra M. Reddy. Institute of Electrical and Electronics Engineers Inc., 2015. pp. 210-215 (Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015).

@inproceedings{90113677489b4c429ca3ee606db0bebb,

title = "Probabilistic formal verification methodology for decentralized thermal management in on-chip systems",

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.",

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",

author = "Shafaq Iqtedar and Osman Hasan and Muhammad Shafique and J{\"o}rg Henkel",

note = "Publisher Copyright: {\textcopyright} 2015 IEEE. Copyright: Copyright 2015 Elsevier B.V., All rights reserved.; 2015 24th IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015 ; Conference date: 15-06-2015 Through 17-06-2015",

year = "2015",

month = aug,

day = "12",

doi = "10.1109/WETICE.2015.39",

language = "English (US)",

series = "Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises, WETICE 2015",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "210--215",

editor = "Reddy, {Sumitra M.}",

booktitle = "Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies",

}

TY - GEN

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

AU - Iqtedar, Shafaq

AU - Hasan, Osman

AU - Shafique, Muhammad

AU - Henkel, Jörg

PY - 2015/8/12

Y1 - 2015/8/12

N2 - 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.

AB - 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.

KW - Approximate model checking

KW - Decentralized dtm scheme

KW - Many core system

KW - Markov chain

KW - Model checking

KW - Power trading agent

KW - Power unit

KW - Probabilistic model checking

KW - Tape dtm scheme

KW - Temperature

KW - Thermal hotspot

UR - http://www.scopus.com/inward/record.url?scp=84943787429&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84943787429&partnerID=8YFLogxK

U2 - 10.1109/WETICE.2015.39

DO - 10.1109/WETICE.2015.39

M3 - Conference contribution

AN - SCOPUS:84943787429

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

SP - 210

EP - 215

BT - Proceedings - 2015 IEEE 24th International Conference on Enabling Technologies

A2 - Reddy, Sumitra M.

PB - Institute of Electrical and Electronics Engineers Inc.

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

Y2 - 15 June 2015 through 17 June 2015

ER -

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this