Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems

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